Theorem rabeqbidv 3410

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

Hypotheses

Ref	Expression
rabeqbidv.1	⊢ (𝜑 → 𝐴 = 𝐵)
rabeqbidv.2	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
rabeqbidv	⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	rabeqdv 3409	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3404	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2778	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539  {crab 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072

This theorem is referenced by:  elfvmptrab1w  6883  elfvmptrab1  6884  fvmptrabfv  6888  elovmporab1w  7494  elovmporab1  7495  ovmpt3rab1  7505  suppval  7950  mpoxopoveq  8006  supeq123d  9139  phival  16396  dfphi2  16403  hashbcval  16631  imasval  17139  ismre  17216  mrisval  17256  isacs  17277  monfval  17361  ismon  17362  monpropd  17366  natfval  17578  isnat  17579  initoval  17624  termoval  17625  gsumvalx  18275  gsumpropd  18277  gsumress  18281  ismhm  18347  issubm  18357  issubg  18670  isnsg  18698  isgim  18793  isga  18812  cntzfval  18841  isslw  19128  isirred  19856  dfrhm2  19876  isrim0  19882  issubrg  19939  issdrg  19978  abvfval  19993  lssset  20110  islmhm  20204  islmim  20239  islbs  20253  rrgval  20471  ocvfval  20783  isobs  20837  dsmmval  20851  islinds  20926  mplval  21107  mhpfval  21239  mplbaspropd  21318  dmatval  21549  scmatval  21561  cpmat  21766  cldval  22082  mretopd  22151  neifval  22158  ordtval  22248  ordtbas2  22250  ordtcnv  22260  ordtrest2  22263  cnfval  22292  cnpfval  22293  kgenval  22594  xkoval  22646  dfac14  22677  qtopval  22754  qtopval2  22755  hmeofval  22817  elmptrab  22886  fgval  22929  flimval  23022  utopval  23292  ucnval  23337  iscfilu  23348  ispsmet  23365  ismet  23384  isxmet  23385  blfvalps  23444  cncfval  23957  ishtpy  24041  isphtpy  24050  om1val  24099  cfilfval  24333  caufval  24344  cpnfval  25001  uc1pval  25209  mon1pval  25211  dchrval  26287  istrkgl  26723  israg  26962  iseqlg  27132  ttgval  27140  nbgrval  27606  vtxdgfval  27737  vtxdeqd  27747  1egrvtxdg1  27779  umgr2v2evd2  27797  wwlks  28101  wwlksn  28103  wspthsn  28114  wwlksnon  28117  wspthsnon  28118  iswspthsnon  28122  rusgrnumwwlklem  28236  clwwlk  28248  clwwlkn  28291  2clwwlk  28612  numclwlk1lem2  28635  numclwwlkovh0  28637  numclwwlkovq  28639  lnoval  29015  bloval  29044  hmoval  29073  mntoval  31162  tocycval  31277  prmidlval  31514  mxidlval  31535  rprmval  31566  ordtprsuni  31771  sigagenval  32008  faeval  32114  ismbfm  32119  carsgval  32170  sitgval  32199  reprval  32490  erdszelem3  33055  erdsze  33064  kur14  33078  iscvm  33121  satf  33215  wlimeq12  33740  leftval  33974  rightval  33975  fwddifval  34391  poimirlem28  35732  istotbnd  35854  isbnd  35865  rngohomval  36049  rngoisoval  36062  idlval  36098  pridlval  36118  maxidlval  36124  igenval  36146  lshpset  36919  lflset  37000  pats  37226  llnset  37446  lplnset  37470  lvolset  37513  lineset  37679  pmapfval  37697  paddfval  37738  lhpset  37936  ldilfset  38049  ltrnfset  38058  ltrnset  38059  dilfsetN  38093  trnfsetN  38096  trnsetN  38097  diaffval  38971  diafval  38972  dicffval  39115  dochffval  39290  lpolsetN  39423  lcdfval  39529  lcdval  39530  mapdffval  39567  mapdfval  39568  isnacs  40442  mzpclval  40463  k0004val  41649  fourierdlem2  43540  fourierdlem3  43541  etransclem12  43677  etransclem33  43698  caragenval  43921  smflimlem3  44195  fvmptrab  44671  iccpval  44755  ismgmhm  45225  issubmgm  45231  assintopval  45287  rnghmval  45337  isrngisom  45342  dmatALTval  45629  lcoop  45640  lines  45965  rrxlines  45967  spheres  45980