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 1569   ∈ wcel 2144  {crab 3412

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

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

This theorem is used by:  elfvmptrab1w  7021  elfvmptrab1  7022  fvmptrabfv  7026  elovmporab1w  7668  elovmporab1  7669  ovmpt3rab1  7679  suppval  8179  mpoxopoveq  8236  supeq123d  9442  phival  16944  dfphi2  16951  hashbcval  17180  imasval  17683  ismre  17760  mrisval  17804  isacs  17825  monfval  17907  ismon  17908  monpropd  17912  natfval  18124  isnat  18125  initoval  18168  termoval  18169  gsumvalx  18865  gsumpropd  18867  gsumress  18871  ismgmhm  18885  issubmgm  18891  ismhm  18980  issubm  18998  issubg  19336  isnsg  19365  isgim  19476  isga  19505  cntzfval  19534  isslw  19822  isirred  20649  rnghmval  20670  isrngim  20675  dfrhm2  20704  rhmval0  20705  isrim0  20713  issubrng  20799  issubrg  20823  rrgval  20949  issdrg  21045  abvfval  21067  lssset  21208  islmhm  21302  islmim  21337  islbs  21351  prmidlval  21618  ocvfval  21972  isobs  22026  dsmmval  22040  islinds  22115  mplval  22296  mhpfval  22459  mplbaspropd  22554  dmatval  22807  scmatval  22819  cpmat  23027  cldval  23341  mretopd  23410  neifval  23417  ordtval  23507  ordtbas2  23509  ordtcnv  23519  ordtrest2  23522  cnfval  23551  cnpfval  23552  kgenval  23854  xkoval  23906  dfac14  23937  qtopval  24014  qtopval2  24015  hmeofval  24077  elmptrab  24146  fgval  24189  flimval  24282  utopval  24551  ucnval  24595  iscfilu  24606  ispsmet  24623  ismet  24642  isxmet  24643  blfvalps  24702  cncfval  25209  ishtpy  25293  isphtpy  25302  om1val  25351  cfilfval  25585  caufval  25596  cpnfval  26252  uc1pval  26458  mon1pval  26460  dchrval  27561  leftval  28235  rightval  28236  istrkgl  28920  israg  29172  tgplnfn  29253  plngval  29255  isplng  29256  iseqlg  29412  ttgval  29452  nbgrval  29917  vtxdgfval  30048  vtxdeqd  30058  1egrvtxdg1  30090  umgr2v2evd2  30108  wwlks  30424  wwlksn  30426  wspthsn  30437  wwlksnon  30440  wspthsnon  30441  iswspthsnon  30445  rusgrnumwwlklem  30562  clwwlk  30574  clwwlkn  30617  2clwwlk  30948  numclwlk1lem2  30971  numclwwlkovh0  30973  numclwwlkovq  30975  lnoval  31354  bloval  31383  hmoval  31412  mntoval  33543  tocycval  33669  fxpval  33726  fldgenval  33874  mxidlval  33986  rprmval  34048  minplyval  34337  ordtprsuni  34551  sigagenval  34773  faeval  34879  ismbfm  34884  carsgval  34935  sitgval  34964  reprval  35239  erdszelem3  35958  erdsze  35967  kur14  35981  iscvm  36024  satf  36118  wlimeq12  36581  fwddifval  36927  poimirlem28  38567  istotbnd  38704  isbnd  38715  rngohomval  38899  rngoisoval  38912  idlval  38948  pridlval  38968  maxidlval  38974  igenval  38996  lshpset  40036  lflset  40117  pats  40343  llnset  40563  lplnset  40587  lvolset  40630  lineset  40796  pmapfval  40814  paddfval  40855  lhpset  41053  ldilfset  41166  ltrnfset  41175  ltrnset  41176  dilfsetN  41210  trnfsetN  41213  trnsetN  41214  diaffval  42088  diafval  42089  dicffval  42232  dochffval  42407  lpolsetN  42540  lcdfval  42646  lcdval  42647  mapdffval  42684  mapdfval  42685  prjcrvfval  43668  isnacs  43715  mzpclval  43736  k0004val  45150  dvnprodlem1  46956  fourierdlem2  47119  fourierdlem3  47120  etransclem12  47256  etransclem33  47277  caragenval  47503  smflimlem3  47783  fvmptrab  48362  iccpval  48497  clnbgrval  48920  isisubgr  48960  grtri  49038  stgrfv  49051  gpgov  49140  assintopval  49302  dmatALTval  49512  lcoop  49523  lines  49843  rrxlines  49845  spheres  49858