Theorem rabeqbidv 3108

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 3107	. . 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 3105	. 2 |- ( ph -> { x e. B | ps } = { x e. B | ch } )
6	3, 5	eqtrd 2508	1 |- ( ph -> { x e. A | ps } = { x e. B | ch } )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1379   {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-nfc 2617  df-ral 2819  df-rab 2823

This theorem is referenced by:  elfvmptrab1  5970  elovmpt2rab1  6506  ovmpt3rab1  6518  suppval  6903  mpt2xopoveq  6947  supeq123d  7910  phival  14156  dfphi2  14163  hashbcval  14379  imasval  14766  ismre  14845  mrisval  14885  isacs  14906  monfval  14988  ismon  14989  monpropd  14993  natfval  15173  isnat  15174  coafval  15249  ismhm  15788  issubm  15797  gsumvalx  15824  gsumpropd  15826  gsumress  15829  issubg  16006  isnsg  16035  isgim  16115  isga  16134  cntzfval  16163  isslw  16434  dprdval  16837  dprdvalOLD  16839  isirred  17149  dfrhm2  17167  isrim0  17173  issubrg  17229  abvfval  17267  lssset  17380  islmhm  17473  islmim  17508  islbs  17522  rrgval  17734  mplval  17883  mplbaspropd  18077  ocvfval  18492  isobs  18546  dsmmval  18560  islinds  18639  dmatval  18789  scmatval  18801  cpmat  19005  cldval  19318  mretopd  19387  neifval  19394  ordtval  19484  ordtbas2  19486  ordtcnv  19496  ordtrest2  19499  cnfval  19528  cnpfval  19529  kgenval  19799  xkoval  19851  dfac14  19882  qtopval  19959  qtopval2  19960  hmeofval  20022  elmptrab  20091  fgval  20134  flimval  20227  utopval  20498  ucnval  20543  iscfilu  20554  ispsmet  20571  ismet  20589  isxmet  20590  blfvalps  20649  cncfval  21155  ishtpy  21235  isphtpy  21244  om1val  21293  cfilfval  21466  caufval  21477  cpnfval  22098  uc1pval  22303  mon1pval  22305  dchrval  23265  istrkgl  23611  israg  23810  ttgval  23882  isausgra  24058  usgraeq12d  24066  usgra0v  24075  usgra1v  24094  nbgraop  24127  isuvtx  24192  wwlk  24385  clwwlk  24470  is2wlkonot  24567  is2spthonot  24568  2wlksot  24571  2spthsot  24572  2wlkonot3v  24579  2spthonot3v  24580  vdgrfval  24599  rusgranumwlklem2  24654  numclwwlkovf  24786  numclwwlkovg  24792  numclwwlkovq  24804  numclwwlkovh  24806  numclwwlk5  24817  lnoval  25371  bloval  25400  hmoval  25429  ordtprsuni  27565  ordtcnvNEW  27566  sigagenval  27808  faeval  27886  ismbfm  27891  sitgval  27942  erdszelem3  28305  erdsze  28314  kur14  28328  iscvm  28372  elgiso  28539  wlimeq12  28980  istotbnd  29896  isbnd  29907  rngohomval  29998  rngoisoval  30011  idlval  30041  pridlval  30061  maxidlval  30067  igenval  30089  isnacs  30268  mzpclval  30289  issdrg  30779  fourierdlem2  31437  fourierdlem3  31438  assintopval  31985  dmatALTval  32100  lcoop  32111  lshpset  33793  lflset  33874  pats  34100  llnset  34319  lplnset  34343  lvolset  34386  lineset  34552  pmapfval  34570  paddfval  34611  pclfvalN  34703  lhpset  34809  ldilfset  34922  ltrnfset  34931  ltrnset  34932  dilfsetN  34966  trnfsetN  34969  trnsetN  34970  diaffval  35845  diafval  35846  dicffval  35989  dochffval  36164  lpolsetN  36297  lcdfval  36403  lcdval  36404  mapdffval  36441  mapdfval  36442