Theorem rabeqbidv 3451

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 480	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒))
4	1, 3	rabeqbidva 3449	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1536   ∈ wcel 2105  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433

This theorem is referenced by:  elfvmptrab1w  7042  elfvmptrab1  7043  fvmptrabfv  7047  elovmporab1w  7679  elovmporab1  7680  ovmpt3rab1  7690  suppval  8185  mpoxopoveq  8242  supeq123d  9487  phival  16800  dfphi2  16807  hashbcval  17035  imasval  17557  ismre  17634  mrisval  17674  isacs  17695  monfval  17779  ismon  17780  monpropd  17784  natfval  18000  isnat  18001  initoval  18046  termoval  18047  gsumvalx  18701  gsumpropd  18703  gsumress  18707  ismgmhm  18721  issubmgm  18727  ismhm  18810  issubm  18828  issubg  19156  isnsg  19185  isgim  19292  isga  19321  cntzfval  19350  isslw  19640  isirred  20435  rnghmval  20456  isrngim  20461  dfrhm2  20490  isrim0OLD  20497  isrim0  20499  issubrng  20563  issubrg  20587  rrgval  20713  issdrg  20805  abvfval  20827  lssset  20948  islmhm  21043  islmim  21078  islbs  21092  ocvfval  21701  isobs  21757  dsmmval  21771  islinds  21846  mplval  22026  mhpfval  22159  mplbaspropd  22253  dmatval  22513  scmatval  22525  cpmat  22730  cldval  23046  mretopd  23115  neifval  23122  ordtval  23212  ordtbas2  23214  ordtcnv  23224  ordtrest2  23227  cnfval  23256  cnpfval  23257  kgenval  23558  xkoval  23610  dfac14  23641  qtopval  23718  qtopval2  23719  hmeofval  23781  elmptrab  23850  fgval  23893  flimval  23986  utopval  24256  ucnval  24301  iscfilu  24312  ispsmet  24329  ismet  24348  isxmet  24349  blfvalps  24408  cncfval  24927  ishtpy  25017  isphtpy  25026  om1val  25076  cfilfval  25311  caufval  25322  cpnfval  25982  uc1pval  26193  mon1pval  26195  dchrval  27292  leftval  27916  rightval  27917  istrkgl  28480  israg  28719  iseqlg  28889  ttgval  28897  ttgvalOLD  28898  nbgrval  29367  vtxdgfval  29499  vtxdeqd  29509  1egrvtxdg1  29541  umgr2v2evd2  29559  wwlks  29864  wwlksn  29866  wspthsn  29877  wwlksnon  29880  wspthsnon  29881  iswspthsnon  29885  rusgrnumwwlklem  29999  clwwlk  30011  clwwlkn  30054  2clwwlk  30375  numclwlk1lem2  30398  numclwwlkovh0  30400  numclwwlkovq  30402  lnoval  30780  bloval  30809  hmoval  30838  mntoval  32956  tocycval  33110  fldgenval  33293  prmidlval  33444  mxidlval  33468  rprmval  33523  minplyval  33712  ordtprsuni  33879  sigagenval  34120  faeval  34226  ismbfm  34231  carsgval  34284  sitgval  34313  reprval  34603  erdszelem3  35177  erdsze  35186  kur14  35200  iscvm  35243  satf  35337  wlimeq12  35800  fwddifval  36143  poimirlem28  37634  istotbnd  37755  isbnd  37766  rngohomval  37950  rngoisoval  37963  idlval  37999  pridlval  38019  maxidlval  38025  igenval  38047  lshpset  38959  lflset  39040  pats  39266  llnset  39487  lplnset  39511  lvolset  39554  lineset  39720  pmapfval  39738  paddfval  39779  lhpset  39977  ldilfset  40090  ltrnfset  40099  ltrnset  40100  dilfsetN  40134  trnfsetN  40137  trnsetN  40138  diaffval  41012  diafval  41013  dicffval  41156  dochffval  41331  lpolsetN  41464  lcdfval  41570  lcdval  41571  mapdffval  41608  mapdfval  41609  prjcrvfval  42617  isnacs  42691  mzpclval  42712  k0004val  44139  dvnprodlem1  45901  fourierdlem2  46064  fourierdlem3  46065  etransclem12  46201  etransclem33  46222  caragenval  46448  smflimlem3  46728  fvmptrab  47241  iccpval  47339  clnbgrval  47746  isisubgr  47785  grtri  47844  stgrfv  47855  gpgov  47936  assintopval  48048  dmatALTval  48245  lcoop  48256  lines  48580  rrxlines  48582  spheres  48595