Theorem rabeqbidv 2962

Description: Equality of restricted class abstractions. (Contributed by Jeff Madsen, 1-Dec-2009.)

Hypotheses

Ref	Expression
rabeqbidv.1	|- ( ph -> A = B )
rabeqbidv.2	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
rabeqbidv	|- ( ph -> { x e. A | ps } = { x e. B | ch } )

Distinct variable groups:   x, A   x, B   ph, x

Allowed substitution hints:   ps( x)   ch( x)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 |- ( ph -> A = B )
2		rabeq 2961	. . 3 |- ( A = B -> { x e. A | ps } = { x e. B | ps } )
3	1, 2	syl 16	. 2 |- ( ph -> { x e. A | ps } = { x e. B | ps } )
4		rabeqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
5	4	rabbidv 2959	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2470	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1369   {crab 2714

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 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rab 2719

This theorem is referenced by:  suppval  6687  mpt2xopoveq  6731  supeq123d  7692  phival  13834  dfphi2  13841  hashbcval  14055  imasval  14441  ismre  14520  mrisval  14560  isacs  14581  monfval  14663  ismon  14664  monpropd  14668  natfval  14848  isnat  14849  coafval  14924  ismhm  15458  issubm  15466  gsumvalx  15493  gsumpropd  15495  gsumress  15498  issubg  15672  isnsg  15701  isgim  15781  isga  15800  cntzfval  15829  isslw  16098  dprdval  16475  dprdvalOLD  16477  isirred  16781  dfrhm2  16798  issubrg  16845  abvfval  16883  lssset  16995  islmhm  17088  islmim  17123  islbs  17137  rrgval  17338  mplval  17481  mplbaspropd  17671  ocvfval  18071  isobs  18125  dsmmval  18139  islinds  18218  cldval  18607  mretopd  18676  neifval  18683  ordtval  18773  ordtbas2  18775  ordtcnv  18785  ordtrest2  18788  cnfval  18817  cnpfval  18818  kgenval  19088  xkoval  19140  dfac14  19171  qtopval  19248  qtopval2  19249  hmeofval  19311  elmptrab  19380  fgval  19423  flimval  19516  utopval  19787  ucnval  19832  iscfilu  19843  ispsmet  19860  ismet  19878  isxmet  19879  blfvalps  19938  cncfval  20444  ishtpy  20524  isphtpy  20533  om1val  20582  cfilfval  20755  caufval  20766  cpnfval  21386  uc1pval  21591  mon1pval  21593  dchrval  22553  istrkgl  22901  israg  23068  ttgval  23089  isausgra  23246  usgraeq12d  23252  usgra0v  23258  usgra1v  23276  nbgraop  23303  isuvtx  23364  vdgrfval  23533  lnoval  24120  bloval  24149  hmoval  24178  ordtprsuni  26318  ordtcnvNEW  26319  sigagenval  26552  faeval  26631  ismbfm  26636  sitgval  26687  erdszelem3  27050  erdsze  27059  kur14  27073  iscvm  27117  elgiso  27284  wlimeq12  27725  istotbnd  28639  isbnd  28650  rngohomval  28741  rngoisoval  28754  idlval  28784  pridlval  28804  maxidlval  28810  igenval  28832  isnacs  29011  mzpclval  29032  issdrg  29525  elfvmptrab1  30125  elovmpt2rab1  30130  ovmpt3rab1  30132  wwlk  30286  is2wlkonot  30353  is2spthonot  30354  2wlksot  30357  2spthsot  30358  2wlkonot3v  30365  2spthonot3v  30366  clwwlk  30400  rusgranumwlklem2  30539  numclwwlkovf  30645  numclwwlkovg  30651  numclwwlkovq  30663  numclwwlkovh  30665  numclwwlk5  30676  lcoop  30876  lshpset  32516  lflset  32597  pats  32823  llnset  33042  lplnset  33066  lvolset  33109  lineset  33275  pmapfval  33293  paddfval  33334  pclfvalN  33426  lhpset  33532  ldilfset  33645  ltrnfset  33654  ltrnset  33655  dilfsetN  33689  trnfsetN  33692  trnsetN  33693  diaffval  34568  diafval  34569  dicffval  34712  dochffval  34887  lpolsetN  35020  lcdfval  35126  lcdval  35127  mapdffval  35164  mapdfval  35165