Theorem rabeqbidv 3077

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 3075	. . 3 |- ( A = B -> { x e. A | ps } = { x e. B | ps } )
3	1, 2	syl 17	. 2 |- ( ph -> { x e. A | ps } = { x e. B | ps } )
4		rabeqbidv.2	. . 3 |- ( ph -> ( ps <-> ch ) )
5	4	rabbidv 3073	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2464	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 188   = wceq 1438   {crab 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-rab 2785

This theorem is referenced by:  elfvmptrab1  5984  elovmpt2rab1  6528  ovmpt3rab1  6537  suppval  6925  mpt2xopoveq  6971  supeq123d  7968  phival  14708  dfphi2  14715  hashbcval  14947  imasval  15404  imasvalOLD  15405  ismre  15489  mrisval  15529  isacs  15550  monfval  15630  ismon  15631  monpropd  15635  natfval  15844  isnat  15845  initoval  15885  termoval  15886  gsumvalx  16506  gsumpropd  16508  gsumress  16512  ismhm  16577  issubm  16587  issubg  16810  isnsg  16839  isgim  16919  isga  16938  cntzfval  16967  isslw  17253  isirred  17920  dfrhm2  17938  isrim0  17944  issubrg  18001  abvfval  18039  lssset  18150  islmhm  18243  islmim  18278  islbs  18292  rrgval  18504  mplval  18645  mplbaspropd  18823  ocvfval  19221  isobs  19275  dsmmval  19289  islinds  19359  dmatval  19509  scmatval  19521  cpmat  19725  cldval  20030  mretopd  20100  neifval  20107  ordtval  20197  ordtbas2  20199  ordtcnv  20209  ordtrest2  20212  cnfval  20241  cnpfval  20242  kgenval  20542  xkoval  20594  dfac14  20625  qtopval  20702  qtopval2  20703  hmeofval  20765  elmptrab  20834  fgval  20877  flimval  20970  utopval  21239  ucnval  21284  iscfilu  21295  ispsmet  21312  ismet  21330  isxmet  21331  blfvalps  21390  cncfval  21912  ishtpy  21995  isphtpy  22004  om1val  22053  cfilfval  22226  caufval  22237  cpnfval  22878  uc1pval  23082  mon1pval  23084  dchrval  24154  istrkgl  24498  israg  24734  iseqlg  24889  ttgval  24897  nbgraop  25143  isuvtx  25208  wwlk  25401  clwwlk  25486  is2wlkonot  25583  is2spthonot  25584  2wlksot  25587  2spthsot  25588  2wlkonot3v  25595  2spthonot3v  25596  vdgrfval  25615  rusgranumwlklem2  25670  numclwwlkovf  25801  numclwwlkovg  25807  numclwwlkovq  25819  numclwwlkovh  25821  numclwwlk5  25832  lnoval  26385  bloval  26414  hmoval  26443  ordtprsuni  28727  sigagenval  28964  faeval  29071  ismbfm  29076  carsgval  29137  sitgval  29167  erdszelem3  29918  erdsze  29927  kur14  29941  iscvm  29984  elgiso  30316  wlimeq12  30503  fwddifval  30928  poimirlem28  31926  istotbnd  32059  isbnd  32070  rngohomval  32161  rngoisoval  32174  idlval  32204  pridlval  32224  maxidlval  32230  igenval  32252  lshpset  32507  lflset  32588  pats  32814  llnset  33033  lplnset  33057  lvolset  33100  lineset  33266  pmapfval  33284  paddfval  33325  lhpset  33523  ldilfset  33636  ltrnfset  33645  ltrnset  33646  dilfsetN  33681  trnfsetN  33684  trnsetN  33685  diaffval  34561  diafval  34562  dicffval  34705  dochffval  34880  lpolsetN  35013  lcdfval  35119  lcdval  35120  mapdffval  35157  mapdfval  35158  isnacs  35509  mzpclval  35530  issdrg  36027  fourierdlem2  37835  fourierdlem3  37836  etransclem12  37975  etransclem33  37996  caragenval  38137  iccpval  38485  ismgmhm  39125  issubmgm  39131  assintopval  39183  rnghmval  39233  isrngisom  39238  dmatALTval  39537  lcoop  39548