Theorem rabbidva 3188

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 2966	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 3120	. 2 |- ( A. x e. A ( ps <-> ch ) <-> { x e. A | ps } = { x e. A | ch } )
4	2, 3	sylib 208	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-rab 2921

This theorem is referenced by:  rabbidv  3189  rabeqbidva  3196  rabbi2dva  3821  rabxfrd  4889  seinxp  5185  ordintdif  5774  f1oresrab  6395  onsucmin  7021  suppval1  7301  mptsuppd  7318  cantnflem1  8586  dfinfre  11004  ixxin  12192  mptnn0fsuppr  12799  scshwfzeqfzo  13572  incexc2  14570  smueqlem  15212  gcdass  15264  lcmass  15327  pcneg  15578  ramval  15712  acsfn  16320  monpropd  16397  f1omvdcnv  17864  pmtrmvd  17876  submod  17984  odngen  17992  sylow3lem6  18047  efgsfo  18152  rrgsupp  19291  mplsubglem2  19436  ltbwe  19472  coe1mul2lem2  19638  dsmmbas2  20081  dsmmacl  20085  frlmbas  20099  frlmsslss2  20114  scmatmats  20317  mretopd  20896  ordtbaslem  20992  ordtrest  21006  ordtrest2lem  21007  leordtval  21017  xkopt  21458  xkoco1cn  21460  xkoco2cn  21461  xkoinjcn  21490  r0cld  21541  utopsnneiplem  22051  stdbdbl  22322  minveclem3b  23199  minveclem4  23203  lhop1lem  23776  mumul  24907  sqff1o  24908  lgsquadlem1  25105  lgsquadlem2  25106  2lgslem1a  25116  edglnl  26038  nbupgr  26240  isuvtxa  26295  vtxdun  26377  wwlksnextprop  26807  wpthswwlks2on  26854  rusgrnumwwlkslem  26864  rusgrnumwwlks  26869  frcond3  27133  extwwlkfab  27223  grpoidinv2  27369  grpoinv  27379  xppreima  29449  cnvordtrestixx  29959  ordtrestNEW  29967  ordtrest2NEWlem  29968  lineunray  32254  lineelsb2  32255  linecom  32257  ee7.2aOLD  32460  poimirlem26  33435  poimirlem27  33436  mbfposadd  33457  cnambfre  33458  itg2addnclem2  33462  iblabsnclem  33473  ftc1anclem1  33485  lfl1dim2N  34409  pmapat  35049  pmapglbx  35055  dvhb1dimN  36274  dia0  36341  mapdval2N  36919  mapdsn  36930  hlhilocv  37249  istopclsd  37263  diophren  37377  rabrenfdioph  37378  pwfi2f1o  37666  acsfn1p  37769  idomrootle  37773  idomodle  37774  hausgraph  37790  fsovcnvlem  38307  ntrneifv3  38380  ntrneifv4  38383  clsneifv3  38408  clsneifv4  38409  neicvgfv  38419  nzss  38516  preimaiocmnf  39788  preimaicomnf  40922  smfsupxr  41022  smfliminflem  41036  sprvalpwle2  41739  rmsupp0  42149  lco0  42216