Theorem rabbidva 3104

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 2878	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 3040	. 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 1379   e. wcel 1767   A.wral 2814   {crab 2818

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-ral 2819  df-rab 2823

This theorem is referenced by:  rabbidv  3105  rabeqbidva  3109  rabbi2dva  3706  rabxfrd  4668  ordintdif  4927  seinxp  5066  f1oresrab  6053  onsucmin  6640  suppval1  6907  mptsuppd  6923  cantnflem1  8108  dfinfmr  10520  ixxin  11546  mptnn0fsuppr  12073  scshwfzeqfzo  12757  incexc2  13613  smueqlem  13999  gcdass  14042  pcneg  14256  ramval  14385  acsfn  14914  monpropd  14993  f1omvdcnv  16275  pmtrmvd  16287  submod  16395  odngen  16403  sylow3lem6  16458  efgsfo  16563  rrgsupp  17738  rrgsuppOLD  17739  mplsubglem2  17896  ltbwe  17936  coe1mul2lem2  18108  dsmmbas2  18563  dsmmacl  18567  frlmbas  18581  frlmbasOLD  18582  frlmsslss2  18600  frlmsslss2OLD  18601  scmatmats  18808  mretopd  19387  ordtbaslem  19483  ordtrest  19497  ordtrest2lem  19498  leordtval  19508  xkopt  19919  xkoco1cn  19921  xkoco2cn  19922  xkoinjcn  19951  r0cld  20002  utopsnneiplem  20513  stdbdbl  20783  minveclem3b  21606  minveclem4  21610  lhop1lem  22177  mumul  23211  sqff1o  23212  lgsquadlem1  23385  lgsquadlem2  23386  wwlkextprop  24448  2pthwlkonot  24589  vdgrun  24605  vdgrfiun  24606  rusgranumwlklem0  24652  rusgranumwlks  24660  frisusgranb  24701  extwwlkfab  24795  grpoidinv2  24924  grpoinv  24933  xppreima  27187  cnvordtrestixx  27559  ordtrestNEW  27567  ordtrest2NEWlem  27568  lineunray  29402  lineelsb2  29403  linecom  29405  ee7.2aOLD  29531  mbfposadd  29667  cnambfre  29668  itg2addnclem2  29672  iblabsnclem  29683  ftc1anclem1  29695  istopclsd  30264  diophren  30379  rabrenfdioph  30380  pwfi2f1o  30676  acsfn1p  30781  idomrootle  30785  idomodle  30786  hausgraph  30805  lcmass  30846  nzss  30850  rmsupp0  32060  lco0  32127  lfl1dim2N  33937  pmapat  34577  pmapglbx  34583  dvhb1dimN  35800  dia0  35867  mapdval2N  36445  mapdsn  36456  hlhilocv  36775