Theorem rabbidva 3100

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 2871	. 2 |- ( ph -> A. x e. A ( ps <-> ch ) )
3		rabbi 3036	. 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 1395   e. wcel 1819   A.wral 2807   {crab 2811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816

This theorem is referenced by:  rabbidv  3101  rabeqbidva  3105  rabbi2dva  3702  rabxfrd  4677  ordintdif  4936  seinxp  5075  f1oresrab  6064  onsucmin  6655  suppval1  6923  mptsuppd  6941  cantnflem1  8125  dfinfmr  10540  ixxin  11571  mptnn0fsuppr  12107  scshwfzeqfzo  12805  incexc2  13661  smueqlem  14151  gcdass  14194  pcneg  14408  ramval  14537  acsfn  15075  monpropd  15152  f1omvdcnv  16595  pmtrmvd  16607  submod  16715  odngen  16723  sylow3lem6  16778  efgsfo  16883  rrgsupp  18065  rrgsuppOLD  18066  mplsubglem2  18223  ltbwe  18263  coe1mul2lem2  18435  dsmmbas2  18894  dsmmacl  18898  frlmbas  18912  frlmbasOLD  18913  frlmsslss2  18931  frlmsslss2OLD  18932  scmatmats  19139  mretopd  19719  ordtbaslem  19815  ordtrest  19829  ordtrest2lem  19830  leordtval  19840  xkopt  20281  xkoco1cn  20283  xkoco2cn  20284  xkoinjcn  20313  r0cld  20364  utopsnneiplem  20875  stdbdbl  21145  minveclem3b  21968  minveclem4  21972  lhop1lem  22539  mumul  23580  sqff1o  23581  lgsquadlem1  23754  lgsquadlem2  23755  wwlkextprop  24870  vdgrun  25027  vdgrfiun  25028  rusgranumwlklem0  25074  rusgranumwlks  25082  frisusgranb  25123  extwwlkfab  25216  grpoidinv2  25346  grpoinv  25355  xppreima  27630  cnvordtrestixx  28048  ordtrestNEW  28056  ordtrest2NEWlem  28057  lineunray  29959  lineelsb2  29960  linecom  29962  ee7.2aOLD  30088  mbfposadd  30224  cnambfre  30225  itg2addnclem2  30229  iblabsnclem  30240  ftc1anclem1  30252  istopclsd  30794  diophren  30909  rabrenfdioph  30910  pwfi2f1o  31206  acsfn1p  31310  idomrootle  31314  idomodle  31315  hausgraph  31334  lcmass  31380  nzss  31384  rmsupp0  33063  lco0  33130  lfl1dim2N  34948  pmapat  35588  pmapglbx  35594  dvhb1dimN  36813  dia0  36880  mapdval2N  37458  mapdsn  37469  hlhilocv  37788