Theorem rabeqbidv 3437

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 3435	1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐵 ∣ 𝜒})

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420

This theorem is used by:  elfvmptrab1w  7021  elfvmptrab1  7022  fvmptrabfv  7026  elovmporab1w  7663  elovmporab1  7664  ovmpt3rab1  7674  suppval  8160  mpoxopoveq  8217  supeq123d  9412  phival  16836  dfphi2  16843  hashbcval  17072  imasval  17575  ismre  17652  mrisval  17696  isacs  17717  monfval  17799  ismon  17800  monpropd  17804  natfval  18016  isnat  18017  initoval  18060  termoval  18061  gsumvalx  18744  gsumpropd  18746  gsumress  18750  ismgmhm  18764  issubmgm  18770  ismhm  18853  issubm  18871  issubg  19202  isnsg  19231  isgim  19342  isga  19371  cntzfval  19400  isslw  19688  isirred  20512  rnghmval  20533  isrngim  20538  dfrhm2  20567  rhmval0  20568  isrim0  20576  issubrng  20661  issubrg  20685  rrgval  20811  issdrg  20906  abvfval  20928  lssset  21069  islmhm  21163  islmim  21198  islbs  21212  prmidlval  21477  ocvfval  21831  isobs  21885  dsmmval  21899  islinds  21974  mplval  22153  mhpfval  22316  mplbaspropd  22411  dmatval  22664  scmatval  22676  cpmat  22881  cldval  23195  mretopd  23264  neifval  23271  ordtval  23361  ordtbas2  23363  ordtcnv  23373  ordtrest2  23376  cnfval  23405  cnpfval  23406  kgenval  23707  xkoval  23759  dfac14  23790  qtopval  23867  qtopval2  23868  hmeofval  23930  elmptrab  23999  fgval  24042  flimval  24135  utopval  24404  ucnval  24448  iscfilu  24459  ispsmet  24476  ismet  24495  isxmet  24496  blfvalps  24555  cncfval  25062  ishtpy  25146  isphtpy  25155  om1val  25204  cfilfval  25438  caufval  25449  cpnfval  26106  uc1pval  26312  mon1pval  26314  dchrval  27413  leftval  28057  rightval  28058  istrkgl  28742  israg  28992  tgplnfn  29072  plngval  29074  isplng  29075  iseqlg  29199  ttgval  29239  nbgrval  29701  vtxdgfval  29832  vtxdeqd  29842  1egrvtxdg1  29874  umgr2v2evd2  29892  wwlks  30199  wwlksn  30201  wspthsn  30212  wwlksnon  30215  wspthsnon  30216  iswspthsnon  30220  rusgrnumwwlklem  30337  clwwlk  30349  clwwlkn  30392  2clwwlk  30713  numclwlk1lem2  30736  numclwwlkovh0  30738  numclwwlkovq  30740  lnoval  31119  bloval  31148  hmoval  31177  mntoval  33315  tocycval  33441  fxpval  33498  fldgenval  33646  mxidlval  33757  rprmval  33819  minplyval  34108  ordtprsuni  34322  sigagenval  34543  faeval  34649  ismbfm  34654  carsgval  34706  sitgval  34735  reprval  35010  erdszelem3  35697  erdsze  35706  kur14  35720  iscvm  35763  satf  35857  wlimeq12  36321  fwddifval  36666  poimirlem28  38331  istotbnd  38452  isbnd  38463  rngohomval  38647  rngoisoval  38660  idlval  38696  pridlval  38716  maxidlval  38722  igenval  38744  lshpset  39784  lflset  39865  pats  40091  llnset  40311  lplnset  40335  lvolset  40378  lineset  40544  pmapfval  40562  paddfval  40603  lhpset  40801  ldilfset  40914  ltrnfset  40923  ltrnset  40924  dilfsetN  40958  trnfsetN  40961  trnsetN  40962  diaffval  41836  diafval  41837  dicffval  41980  dochffval  42155  lpolsetN  42288  lcdfval  42394  lcdval  42395  mapdffval  42432  mapdfval  42433  prjcrvfval  43395  isnacs  43467  mzpclval  43488  k0004val  44908  dvnprodlem1  46692  fourierdlem2  46855  fourierdlem3  46856  etransclem12  46992  etransclem33  47013  caragenval  47239  smflimlem3  47519  fvmptrab  48061  iccpval  48196  clnbgrval  48619  isisubgr  48659  grtri  48737  stgrfv  48750  gpgov  48839  assintopval  49002  dmatALTval  49212  lcoop  49223  lines  49543  rrxlines  49545  spheres  49558