Theorem rabeqbidv 3421

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 3420	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜓})
3		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
4	3	rabbidv 3415	. 2 ⊢ (𝜑 → {𝑥 ∈ 𝐵 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})
5	2, 4	eqtrd 2779	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074

This theorem is referenced by:  elfvmptrab1w  6910  elfvmptrab1  6911  fvmptrabfv  6915  elovmporab1w  7525  elovmporab1  7526  ovmpt3rab1  7536  suppval  7988  mpoxopoveq  8044  supeq123d  9218  phival  16477  dfphi2  16484  hashbcval  16712  imasval  17231  ismre  17308  mrisval  17348  isacs  17369  monfval  17453  ismon  17454  monpropd  17458  natfval  17671  isnat  17672  initoval  17717  termoval  17718  gsumvalx  18369  gsumpropd  18371  gsumress  18375  ismhm  18441  issubm  18451  issubg  18764  isnsg  18792  isgim  18887  isga  18906  cntzfval  18935  isslw  19222  isirred  19950  dfrhm2  19970  isrim0  19976  issubrg  20033  issdrg  20072  abvfval  20087  lssset  20204  islmhm  20298  islmim  20333  islbs  20347  rrgval  20567  ocvfval  20880  isobs  20936  dsmmval  20950  islinds  21025  mplval  21206  mhpfval  21338  mplbaspropd  21417  dmatval  21650  scmatval  21662  cpmat  21867  cldval  22183  mretopd  22252  neifval  22259  ordtval  22349  ordtbas2  22351  ordtcnv  22361  ordtrest2  22364  cnfval  22393  cnpfval  22394  kgenval  22695  xkoval  22747  dfac14  22778  qtopval  22855  qtopval2  22856  hmeofval  22918  elmptrab  22987  fgval  23030  flimval  23123  utopval  23393  ucnval  23438  iscfilu  23449  ispsmet  23466  ismet  23485  isxmet  23486  blfvalps  23545  cncfval  24060  ishtpy  24144  isphtpy  24153  om1val  24202  cfilfval  24437  caufval  24448  cpnfval  25105  uc1pval  25313  mon1pval  25315  dchrval  26391  istrkgl  26828  israg  27067  iseqlg  27237  ttgval  27245  ttgvalOLD  27246  nbgrval  27712  vtxdgfval  27843  vtxdeqd  27853  1egrvtxdg1  27885  umgr2v2evd2  27903  wwlks  28209  wwlksn  28211  wspthsn  28222  wwlksnon  28225  wspthsnon  28226  iswspthsnon  28230  rusgrnumwwlklem  28344  clwwlk  28356  clwwlkn  28399  2clwwlk  28720  numclwlk1lem2  28743  numclwwlkovh0  28745  numclwwlkovq  28747  lnoval  29123  bloval  29152  hmoval  29181  mntoval  31269  tocycval  31384  prmidlval  31621  mxidlval  31642  rprmval  31673  ordtprsuni  31878  sigagenval  32117  faeval  32223  ismbfm  32228  carsgval  32279  sitgval  32308  reprval  32599  erdszelem3  33164  erdsze  33173  kur14  33187  iscvm  33230  satf  33324  wlimeq12  33822  leftval  34056  rightval  34057  fwddifval  34473  poimirlem28  35814  istotbnd  35936  isbnd  35947  rngohomval  36131  rngoisoval  36144  idlval  36180  pridlval  36200  maxidlval  36206  igenval  36228  lshpset  36999  lflset  37080  pats  37306  llnset  37526  lplnset  37550  lvolset  37593  lineset  37759  pmapfval  37777  paddfval  37818  lhpset  38016  ldilfset  38129  ltrnfset  38138  ltrnset  38139  dilfsetN  38173  trnfsetN  38176  trnsetN  38177  diaffval  39051  diafval  39052  dicffval  39195  dochffval  39370  lpolsetN  39503  lcdfval  39609  lcdval  39610  mapdffval  39647  mapdfval  39648  prjcrvfval  40475  isnacs  40533  mzpclval  40554  k0004val  41767  fourierdlem2  43657  fourierdlem3  43658  etransclem12  43794  etransclem33  43815  caragenval  44038  smflimlem3  44318  fvmptrab  44795  iccpval  44878  ismgmhm  45348  issubmgm  45354  assintopval  45410  rnghmval  45460  isrngisom  45465  dmatALTval  45752  lcoop  45763  lines  46088  rrxlines  46090  spheres  46103