Theorem rabeqbidv 3071

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1370   {crab 2802

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rab 2807

This theorem is referenced by:  suppval  6801  mpt2xopoveq  6845  supeq123d  7810  phival  13959  dfphi2  13966  hashbcval  14180  imasval  14567  ismre  14646  mrisval  14686  isacs  14707  monfval  14789  ismon  14790  monpropd  14794  natfval  14974  isnat  14975  coafval  15050  ismhm  15584  issubm  15593  gsumvalx  15620  gsumpropd  15622  gsumress  15625  issubg  15799  isnsg  15828  isgim  15908  isga  15927  cntzfval  15956  isslw  16227  dprdval  16606  dprdvalOLD  16608  isirred  16913  dfrhm2  16930  isrim0  16935  issubrg  16987  abvfval  17025  lssset  17137  islmhm  17230  islmim  17265  islbs  17279  rrgval  17480  mplval  17624  mplbaspropd  17814  ocvfval  18215  isobs  18269  dsmmval  18283  islinds  18362  cldval  18758  mretopd  18827  neifval  18834  ordtval  18924  ordtbas2  18926  ordtcnv  18936  ordtrest2  18939  cnfval  18968  cnpfval  18969  kgenval  19239  xkoval  19291  dfac14  19322  qtopval  19399  qtopval2  19400  hmeofval  19462  elmptrab  19531  fgval  19574  flimval  19667  utopval  19938  ucnval  19983  iscfilu  19994  ispsmet  20011  ismet  20029  isxmet  20030  blfvalps  20089  cncfval  20595  ishtpy  20675  isphtpy  20684  om1val  20733  cfilfval  20906  caufval  20917  cpnfval  21538  uc1pval  21743  mon1pval  21745  dchrval  22705  istrkgl  23051  israg  23233  ttgval  23272  isausgra  23429  usgraeq12d  23435  usgra0v  23441  usgra1v  23459  nbgraop  23486  isuvtx  23547  vdgrfval  23716  lnoval  24303  bloval  24332  hmoval  24361  ordtprsuni  26493  ordtcnvNEW  26494  sigagenval  26727  faeval  26805  ismbfm  26810  sitgval  26861  erdszelem3  27224  erdsze  27233  kur14  27247  iscvm  27291  elgiso  27458  wlimeq12  27899  istotbnd  28815  isbnd  28826  rngohomval  28917  rngoisoval  28930  idlval  28960  pridlval  28980  maxidlval  28986  igenval  29008  isnacs  29187  mzpclval  29208  issdrg  29701  elfvmptrab1  30301  elovmpt2rab1  30306  ovmpt3rab1  30308  wwlk  30462  is2wlkonot  30529  is2spthonot  30530  2wlksot  30533  2spthsot  30534  2wlkonot3v  30541  2spthonot3v  30542  clwwlk  30576  rusgranumwlklem2  30715  numclwwlkovf  30821  numclwwlkovg  30827  numclwwlkovq  30839  numclwwlkovh  30841  numclwwlk5  30852  lcoop  31063  cpmat  31184  lshpset  32946  lflset  33027  pats  33253  llnset  33472  lplnset  33496  lvolset  33539  lineset  33705  pmapfval  33723  paddfval  33764  pclfvalN  33856  lhpset  33962  ldilfset  34075  ltrnfset  34084  ltrnset  34085  dilfsetN  34119  trnfsetN  34122  trnsetN  34123  diaffval  34998  diafval  34999  dicffval  35142  dochffval  35317  lpolsetN  35450  lcdfval  35556  lcdval  35557  mapdffval  35594  mapdfval  35595