Theorem rabbidva 3050

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

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1405   e. wcel 1842   A.wral 2754   {crab 2758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-ral 2759  df-rab 2763

This theorem is referenced by:  rabbidv  3051  rabeqbidva  3055  rabbi2dva  3647  rabxfrd  4612  seinxp  4890  ordintdif  5459  f1oresrab  6042  onsucmin  6639  suppval1  6908  mptsuppd  6926  cantnflem1  8140  dfinfmr  10560  ixxin  11599  mptnn0fsuppr  12149  scshwfzeqfzo  12850  incexc2  13801  smueqlem  14349  gcdass  14392  pcneg  14606  ramval  14735  acsfn  15273  monpropd  15350  f1omvdcnv  16793  pmtrmvd  16805  submod  16913  odngen  16921  sylow3lem6  16976  efgsfo  17081  rrgsupp  18259  rrgsuppOLD  18260  mplsubglem2  18417  ltbwe  18457  coe1mul2lem2  18629  dsmmbas2  19066  dsmmacl  19070  frlmbas  19084  frlmbasOLD  19085  frlmsslss2  19101  frlmsslss2OLD  19102  scmatmats  19305  mretopd  19886  ordtbaslem  19982  ordtrest  19996  ordtrest2lem  19997  leordtval  20007  xkopt  20448  xkoco1cn  20450  xkoco2cn  20451  xkoinjcn  20480  r0cld  20531  utopsnneiplem  21042  stdbdbl  21312  minveclem3b  22135  minveclem4  22139  lhop1lem  22706  mumul  23836  sqff1o  23837  lgsquadlem1  24010  lgsquadlem2  24011  wwlkextprop  25161  vdgrun  25318  vdgrfiun  25319  rusgranumwlklem0  25365  rusgranumwlks  25373  frisusgranb  25414  extwwlkfab  25507  grpoidinv2  25634  grpoinv  25643  xppreima  27930  cnvordtrestixx  28348  ordtrestNEW  28356  ordtrest2NEWlem  28357  lineunray  30485  lineelsb2  30486  linecom  30488  ee7.2aOLD  30693  mbfposadd  31434  cnambfre  31435  itg2addnclem2  31440  iblabsnclem  31451  ftc1anclem1  31463  lfl1dim2N  32140  pmapat  32780  pmapglbx  32786  dvhb1dimN  34005  dia0  34072  mapdval2N  34650  mapdsn  34661  hlhilocv  34980  istopclsd  34994  diophren  35108  rabrenfdioph  35109  pwfi2f1o  35406  pwfi2f1oOLD  35407  acsfn1p  35512  idomrootle  35516  idomodle  35517  hausgraph  35536  lcmass  36066  nzss  36070  rmsupp0  38472  lco0  38539