Theorem rabeqbidv 3429

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 group:   𝜑,𝑥

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

Proof of Theorem rabeqbidv

Step	Hyp	Ref	Expression
1		rabeqbidv.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		rabeqbidv.2	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	2	adantr 486	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	rabeqbidva 3428	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   ∈ wcel 2145  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413

This theorem is used by:  elfvmptrab1w  7010  elfvmptrab1  7011  fvmptrabfv  7015  elovmporab1w  7657  elovmporab1  7658  ovmpt3rab1  7668  suppval  8158  mpoxopoveq  8215  supeq123d  9420  phival  16891  dfphi2  16898  hashbcval  17127  imasval  17630  ismre  17707  mrisval  17751  isacs  17772  monfval  17854  ismon  17855  monpropd  17859  natfval  18071  isnat  18072  initoval  18115  termoval  18116  gsumvalx  18812  gsumpropd  18814  gsumress  18818  ismgmhm  18832  issubmgm  18838  ismhm  18927  issubm  18945  issubg  19283  isnsg  19312  isgim  19423  isga  19452  cntzfval  19481  isslw  19769  isirred  20596  rnghmval  20617  isrngim  20622  dfrhm2  20651  rhmval0  20652  isrim0  20660  issubrng  20746  issubrg  20770  rrgval  20896  issdrg  20992  abvfval  21014  lssset  21155  islmhm  21249  islmim  21284  islbs  21298  prmidlval  21565  ocvfval  21919  isobs  21973  dsmmval  21987  islinds  22062  mplval  22243  mhpfval  22406  mplbaspropd  22501  dmatval  22754  scmatval  22766  cpmat  22974  cldval  23288  mretopd  23357  neifval  23364  ordtval  23454  ordtbas2  23456  ordtcnv  23466  ordtrest2  23469  cnfval  23498  cnpfval  23499  kgenval  23801  xkoval  23853  dfac14  23884  qtopval  23961  qtopval2  23962  hmeofval  24024  elmptrab  24093  fgval  24136  flimval  24229  utopval  24498  ucnval  24542  iscfilu  24553  ispsmet  24570  ismet  24589  isxmet  24590  blfvalps  24649  cncfval  25156  ishtpy  25240  isphtpy  25249  om1val  25298  cfilfval  25532  caufval  25543  cpnfval  26199  uc1pval  26405  mon1pval  26407  dchrval  27510  leftval  28154  rightval  28155  istrkgl  28839  israg  29091  tgplnfn  29172  plngval  29174  isplng  29175  iseqlg  29331  ttgval  29371  nbgrval  29836  vtxdgfval  29967  vtxdeqd  29977  1egrvtxdg1  30009  umgr2v2evd2  30027  wwlks  30343  wwlksn  30345  wspthsn  30356  wwlksnon  30359  wspthsnon  30360  iswspthsnon  30364  rusgrnumwwlklem  30481  clwwlk  30493  clwwlkn  30536  2clwwlk  30867  numclwlk1lem2  30890  numclwwlkovh0  30892  numclwwlkovq  30894  lnoval  31273  bloval  31302  hmoval  31331  mntoval  33462  tocycval  33588  fxpval  33645  fldgenval  33793  mxidlval  33905  rprmval  33967  minplyval  34256  ordtprsuni  34470  sigagenval  34692  faeval  34798  ismbfm  34803  carsgval  34855  sitgval  34884  reprval  35159  erdszelem3  35873  erdsze  35882  kur14  35896  iscvm  35939  satf  36033  wlimeq12  36497  fwddifval  36843  poimirlem28  38480  istotbnd  38617  isbnd  38628  rngohomval  38812  rngoisoval  38825  idlval  38861  pridlval  38881  maxidlval  38887  igenval  38909  lshpset  39949  lflset  40030  pats  40256  llnset  40476  lplnset  40500  lvolset  40543  lineset  40709  pmapfval  40727  paddfval  40768  lhpset  40966  ldilfset  41079  ltrnfset  41088  ltrnset  41089  dilfsetN  41123  trnfsetN  41126  trnsetN  41127  diaffval  42001  diafval  42002  dicffval  42145  dochffval  42320  lpolsetN  42453  lcdfval  42559  lcdval  42560  mapdffval  42597  mapdfval  42598  prjcrvfval  43575  isnacs  43647  mzpclval  43668  k0004val  45088  dvnprodlem1  46872  fourierdlem2  47035  fourierdlem3  47036  etransclem12  47172  etransclem33  47193  caragenval  47419  smflimlem3  47699  fvmptrab  48278  iccpval  48413  clnbgrval  48836  isisubgr  48876  grtri  48954  stgrfv  48967  gpgov  49056  assintopval  49218  dmatALTval  49428  lcoop  49439  lines  49759  rrxlines  49761  spheres  49774