Theorem rabbidva 3047

Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.)

Hypothesis

Ref	Expression
rabbidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rabbidva

Step	Hyp	Ref	Expression
1		rabbidva.1	. . 3 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
2	1	ralrimiva 2814	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 2981	. 2 |- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
4	2, 3	sylib 201	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1455   e. wcel 1898   A.wral 2749   {crab 2753

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-ral 2754  df-rab 2758

This theorem is referenced by:  rabbidv  3048  rabeqbidva  3053  rabbi2dva  3652  rabxfrd  4638  seinxp  4923  ordintdif  5495  f1oresrab  6084  onsucmin  6680  suppval1  6952  mptsuppd  6970  cantnflem1  8225  dfinfre  10621  dfinfmrOLD  10622  ixxin  11686  mptnn0fsuppr  12249  scshwfzeqfzo  12968  incexc2  13951  smueqlem  14519  gcdass  14568  lcmass  14634  pcneg  14878  ramval  15015  ramvalOLD  15016  acsfn  15620  monpropd  15697  f1omvdcnv  17140  pmtrmvd  17152  submod  17273  odngen  17281  sylow3lem6  17339  efgsfo  17444  rrgsupp  18570  mplsubglem2  18715  ltbwe  18751  coe1mul2lem2  18916  dsmmbas2  19355  dsmmacl  19359  frlmbas  19373  frlmsslss2  19388  scmatmats  19591  mretopd  20163  ordtbaslem  20259  ordtrest  20273  ordtrest2lem  20274  leordtval  20284  xkopt  20725  xkoco1cn  20727  xkoco2cn  20728  xkoinjcn  20757  r0cld  20808  utopsnneiplem  21317  stdbdbl  21587  minveclem3b  22425  minveclem4  22429  minveclem3bOLD  22437  minveclem4OLD  22441  lhop1lem  23021  mumul  24164  sqff1o  24165  lgsquadlem1  24338  lgsquadlem2  24339  wwlkextprop  25528  vdgrun  25685  vdgrfiun  25686  rusgranumwlklem0  25732  rusgranumwlks  25740  frisusgranb  25781  extwwlkfab  25874  grpoidinv2  26002  grpoinv  26011  xppreima  28301  cnvordtrestixx  28770  ordtrestNEW  28778  ordtrest2NEWlem  28779  lineunray  30964  lineelsb2  30965  linecom  30967  ee7.2aOLD  31171  poimirlem26  32012  poimirlem27  32013  mbfposadd  32034  cnambfre  32035  itg2addnclem2  32040  iblabsnclem  32051  ftc1anclem1  32063  lfl1dim2N  32734  pmapat  33374  pmapglbx  33380  dvhb1dimN  34599  dia0  34666  mapdval2N  35244  mapdsn  35255  hlhilocv  35574  istopclsd  35588  diophren  35702  rabrenfdioph  35703  pwfi2f1o  36000  acsfn1p  36111  idomrootle  36115  idomodle  36116  hausgraph  36135  nzss  36711  nbupgr  39558  isuvtxa  39613  vtxduhgrun  39684  rmsupp0  40522  lco0  40589