Theorem rabbidv 2287

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

Hypothesis

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

Assertion

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

Distinct variable group:   ph,x

Proof of Theorem rabbidv

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

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   e. wcel 1300  {crab 2108

This theorem is referenced by:  rabeqbidv 2290  difeq2 2719  supeq1 5665  ordtypelem1 5684  ordtypelem4 5687  ordtypelem5 5688  ordtypelem6 5689  ordtypelem7 5690  ordtype 5691  hartog 5693  inf3lema 5715  tz9.12lem1 5770  tz9.12lem3 5772  rankval 5779  rankvalg 5780  rankonid 5806  oncardval 5865  alephon 5876  omsubsuc 5877  zorn2lem1 5950  zorn2lem6 5955  zorn2lem7 5956  zorn2 5958  cardval 5975  alephsuc 6014  alephsuc2 6029  peano5uzti 7416  flval 7464  iooval 7533  iocval 7542  icoval 7543  iccval 7544  uzval 7588  fzval 7639  seqzfval 7780  sqrval 7921  reval 8005  imval 8006  acdc3lem 8754  acdc3 8755  acdc2lem1 8757  acdc2 8759  acdc5lem1 8760  acdc5 8762  acdclem 8763  acdc 8764  ntrval 8952  clsval 8953  cnfval 9032  cnpfval 9033  cnpval 9035  blfval 9112  blval 9114  grpidval 9342  grpinvfval 9350  grpinvval 9351  issubg 9425  addinv 9436  sspval 9721  bloval 9781  hmoval 9810  ubthlem1 9872  spwval2 9996  spwval 10002  spwpr4 10006  spwpr4OLD 10007  spwpr4aOLD 10008  fgf 10283  sfvlim 10296  limfil 10297  idrval 10374  ocval 10786  pjval 10872  shsumval 10910  spanval 10932  hsupval2 10933  chsupid 10944  nlfnval 11445  eigvecval 11459  specval 11461  cnlnadjlem4 11640  nmopadjlei 11658  hmopidmch 11725  hmopidmpj 11726  cdj3lem2 12007  bnj602 13303  elgiso 13639  isprm2lem 13774  ubos2 14598  ubos 14599  supdef 14604  rngunval2 14774  istopx 14918  limfillem1 14938  limfillem2 14939  cinvlem1 15176  cinvlem2 15177  issubcat 15193  isseg2 15305  isplibg4a 15315  isplibg4b 15317  ordtypelem1OLD 15375  ordtypelem4OLD 15378  ordtypelem5OLD 15379  ordtypelem6OLD 15380  ordtypelem7OLD 15381  ordtypeOLD 15382  hartogOLD 15384  omsubsucOLD 15386  ptfinfin 15508  finlocfin 15509  locfincomp 15514  locfindsc 15515  ist1-3 15543  filssufil 15571  rabeq12OLD 15665  supeq2 15760  phtpyval 16047  pi1fval 16092  igenval 16209  plusssval 17205  ocvval 17207  islinei 17221  pmapval 17237  paddval 17259  paddcom 17274  dilset 17402

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-rab 2112

Copyright terms: Public domain