Theorem rabbidva 2968

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 2804	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 2904	. 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 369   = wceq 1369   e. wcel 1756   A.wral 2720   {crab 2724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-ral 2725  df-rab 2729

This theorem is referenced by:  rabbidv  2969  rabeqbidva  2973  rabbi2dva  3563  rabxfrd  4518  ordintdif  4773  seinxp  4910  f1oresrab  5880  onsucmin  6437  suppval1  6701  mptsuppd  6717  cantnflem1  7902  dfinfmr  10312  ixxin  11322  incexc2  13306  smueqlem  13691  gcdass  13734  pcneg  13945  ramval  14074  acsfn  14602  monpropd  14681  f1omvdcnv  15955  pmtrmvd  15967  submod  16073  odngen  16081  sylow3lem6  16136  efgsfo  16241  rrgsupp  17367  rrgsuppOLD  17368  mplsubglem2  17519  ltbwe  17559  coe1mul2lem2  17727  dsmmbas2  18167  dsmmacl  18171  frlmbas  18185  frlmbasOLD  18186  frlmsslss2  18204  frlmsslss2OLD  18205  mretopd  18701  ordtbaslem  18797  ordtrest  18811  ordtrest2lem  18812  leordtval  18822  xkopt  19233  xkoco1cn  19235  xkoco2cn  19236  xkoinjcn  19265  r0cld  19316  utopsnneiplem  19827  stdbdbl  20097  minveclem3b  20920  minveclem4  20924  lhop1lem  21490  mumul  22524  sqff1o  22525  lgsquadlem1  22698  lgsquadlem2  22699  vdgrun  23576  vdgrfiun  23577  grpoidinv2  23710  grpoinv  23719  xppreima  25969  cnvordtrestixx  26348  ordtrestNEW  26356  ordtrest2NEWlem  26357  lineunray  28183  lineelsb2  28184  linecom  28186  ee7.2aOLD  28312  mbfposadd  28444  cnambfre  28445  itg2addnclem2  28449  iblabsnclem  28460  ftc1anclem1  28472  istopclsd  29041  diophren  29157  rabrenfdioph  29158  pwfi2f1o  29456  acsfn1p  29561  idomrootle  29565  idomodle  29566  hausgraph  29585  2pthwlkonot  30409  scshwfzeqfzo  30497  wwlkextprop  30568  rusgranumwlklem0  30571  rusgranumwlks  30579  frisusgranb  30594  extwwlkfab  30688  rmsupp0  30786  lco0  30966  lfl1dim2N  32772  pmapat  33412  pmapglbx  33418  dvhb1dimN  34635  dia0  34702  mapdval2N  35280  mapdsn  35291  hlhilocv  35610