Theorem rabeqbidv 3026

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   {crab 2760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-rab 2765

This theorem is referenced by:  elfvmptrab1  5985  elovmpt2rab1  6535  ovmpt3rab1  6544  suppval  6935  mpt2xopoveq  6984  supeq123d  7982  phival  14794  dfphi2  14801  hashbcval  15033  imasval  15489  imasvalOLD  15490  ismre  15574  mrisval  15614  isacs  15635  monfval  15715  ismon  15716  monpropd  15720  natfval  15929  isnat  15930  initoval  15970  termoval  15971  gsumvalx  16591  gsumpropd  16593  gsumress  16597  ismhm  16662  issubm  16672  issubg  16895  isnsg  16924  isgim  17004  isga  17023  cntzfval  17052  isslw  17338  isirred  18005  dfrhm2  18023  isrim0  18029  issubrg  18086  abvfval  18124  lssset  18235  islmhm  18328  islmim  18363  islbs  18377  rrgval  18588  mplval  18729  mplbaspropd  18907  ocvfval  19306  isobs  19360  dsmmval  19374  islinds  19444  dmatval  19594  scmatval  19606  cpmat  19810  cldval  20115  mretopd  20185  neifval  20192  ordtval  20282  ordtbas2  20284  ordtcnv  20294  ordtrest2  20297  cnfval  20326  cnpfval  20327  kgenval  20627  xkoval  20679  dfac14  20710  qtopval  20787  qtopval2  20788  hmeofval  20850  elmptrab  20919  fgval  20963  flimval  21056  utopval  21325  ucnval  21370  iscfilu  21381  ispsmet  21398  ismet  21416  isxmet  21417  blfvalps  21476  cncfval  21998  ishtpy  22081  isphtpy  22090  om1val  22139  cfilfval  22312  caufval  22323  cpnfval  22965  uc1pval  23169  mon1pval  23171  dchrval  24241  istrkgl  24585  israg  24821  iseqlg  24976  ttgval  24984  nbgraop  25230  isuvtx  25295  wwlk  25488  clwwlk  25573  is2wlkonot  25670  is2spthonot  25671  2wlksot  25674  2spthsot  25675  2wlkonot3v  25682  2spthonot3v  25683  vdgrfval  25702  rusgranumwlklem2  25757  numclwwlkovf  25888  numclwwlkovg  25894  numclwwlkovq  25906  numclwwlkovh  25908  numclwwlk5  25919  lnoval  26474  bloval  26503  hmoval  26532  ordtprsuni  28799  sigagenval  29036  faeval  29142  ismbfm  29147  carsgval  29208  sitgval  29238  erdszelem3  29988  erdsze  29997  kur14  30011  iscvm  30054  elgiso  30386  wlimeq12  30573  fwddifval  31000  poimirlem28  32032  istotbnd  32165  isbnd  32176  rngohomval  32267  rngoisoval  32280  idlval  32310  pridlval  32330  maxidlval  32336  igenval  32358  lshpset  32615  lflset  32696  pats  32922  llnset  33141  lplnset  33165  lvolset  33208  lineset  33374  pmapfval  33392  paddfval  33433  lhpset  33631  ldilfset  33744  ltrnfset  33753  ltrnset  33754  dilfsetN  33789  trnfsetN  33792  trnsetN  33793  diaffval  34669  diafval  34670  dicffval  34813  dochffval  34988  lpolsetN  35121  lcdfval  35227  lcdval  35228  mapdffval  35265  mapdfval  35266  isnacs  35617  mzpclval  35638  issdrg  36134  fourierdlem2  38083  fourierdlem3  38084  etransclem12  38223  etransclem33  38244  caragenval  38433  iccpval  38874  nbgrval  39570  uvtxaval  39623  vtxdgfval  39693  vtxdeqd  39702  1egrvtxdg1  39732  umgr2v2evd2  39750  ismgmhm  40291  issubmgm  40297  assintopval  40349  rnghmval  40399  isrngisom  40404  dmatALTval  40701  lcoop  40712