Theorem rabbisdv 1803

Description: Equivalent wff's yield equal restricted class abstractions (deduction rule).

Hypothesis

Ref	Expression
rabbisdv.1	|- (ph -> (ps <-> ch))

Assertion

Ref	Expression
rabbisdv	|- (ph -> {x e. A | ps} = {x e. A | ch})

Distinct variable group:   ph,x

Proof of Theorem rabbisdv

Step	Hyp	Ref	Expression
1		rabbisdv.1	. . 3 |- (ph -> (ps <-> ch))
2	1	adantr 389	. 2 |- ((ph /\ x e. A) -> (ps <-> ch))
3	2	rabbidv 1802	1 |- (ph -> {x e. A | ps} = {x e. A | ch})

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956  {crab 1645

This theorem is referenced by:  supeq1 4555  inf3lema 4589  tz9.12lem1 4639  tz9.12lem3 4641  rankval 4648  rankvalg 4649  rankonid 4675  zorn2lem1 4768  zorn2lem6 4773  zorn2lem7 4774  zorn2 4776  oncardval 4799  cardval 4806  alephon 4845  alephsuc 4846  alephsuc2 4861  subvalt 5337  divval 5681  peano5uzt 6160  flvalt 6181  ioovalt 6311  iocvalt 6320  icovalt 6321  iccvalt 6322  uzvalt 6359  fzvalt 6409  seqzfval 6477  sqrval 6609  revalt 6694  imvalt 6695  acdc3lem 7436  acdc3 7437  acdc2lem1 7438  acdc2 7440  acdc5lem1 7441  acdc5 7443  acdclem 7444  acdc 7445  ntrval 7626  clsval 7627  cnfval 7706  cnpfval 7707  cnpval 7709  blfval 7787  blval 7789  grpidval 8008  grpinvfval 8016  grpinvval 8017  issubg 8068  sspval 8329  bloval 8386  hmoval 8414  ubthlem1 8473  spwval2 8595  spwval 8600  ocvalt 9092  pjvalt 9177  shsumvalt 9215  spanvalt 9237  hsupval2t 9238  chsupid 9249  nlfnvalt 9748  eigvecvalt 9762  specvalt 9764  cnlnadjlem4 9941  nmopadjle 9959  hmopidmcht 10019  hmopidmpjt 10020  cdj3lem2 10296  elgiso 10332

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-rab 1649

Copyright terms: Public domain