Theorem eleq1i 2852

Description: Inference from equality to equivalence of membership. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
eleq1i	⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Proof of Theorem eleq1i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		eleq1 2849	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

Syntax hints:   ↔ wb 208   = wceq 1559   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-clel 2836

This theorem is referenced by:  eleq12i  2854  eqeltri  2857  eqneltri  2880  intexrab  5300  abssexg  5336  rmorabex  5424  otelxp  5687  xpsspw  5778  dfse2  6085  dfse3  6318  ordtri3or  6373  fressnfv  7138  fnotovb  7443  ovmpos  7539  abnex  7735  sucexb  7782  f1stres  7989  f2ndres  7990  elxp6  7999  ottpos  8210  dftpos4  8219  tfr2b  8361  tz7.48-3  8409  unfi  9133  difinf  9249  fiint  9265  infssuni  9283  fsuppunbi  9329  r1pwALT  9798  djuexb  9861  alephprc  10049  fin1a2lem12  10362  axcclem  10408  zorn2lem4  10450  zornn0g  10456  grothomex  10781  grothprimlem  10785  addclprlem2  10969  axicn  11102  0mnnnnn0  12507  fcdmnn0fsupp  12533  pfxccatin12lem3  14739  pfxccat3  14741  swrdccat  14742  pfxccat3a  14745  swrdccat3blem  14746  swrdccat3b  14747  harmonic  15880  nprmi  16714  issubmgm  18727  issubm  18828  idresefmnd  18924  mulgfval  19102  oppgsubm  19393  idrespermg  19442  issrg  20225  srgfcl  20233  subrngrng  20587  opprsubrng  20596  rhmimasubrng  20603  cntzsubrng  20604  opprsubrg  20630  rngridlmcl  21275  isridlrng  21277  isridl  21310  resubdrg  21648  cpmidpmat  22921  kgencn  23604  kgencn2  23605  txdis1cn  23683  qtopres  23746  qtopcn  23762  cfinfil  23941  tgphaus  24165  xmeterval  24480  blval2  24610  metuel2  24613  iscvsp  25178  zclmncvs  25198  caucfil  25333  resscdrg  25408  finiunmbl  25594  iblre  25844  dvfsumlem2  26077  logno1  26689  rlimcnp2  27019  ppi2i  27221  gausslemma2dlem1a  27417  2lgslem4  27458  noxp1o  27715  usgrexmpl  29421  usgredgffibi  29482  nbupgrel  29503  nbuhgr2vtx1edgb  29510  nbusgreledg  29511  nbusgrf1o0  29527  nb3grpr  29540  nb3grpr2  29541  nb3gr2nb  29542  cusgrsizeinds  29610  cusgrfi  29616  finsumvtxdg2size  29708  wlkp1lem1  29829  wlkp1lem7  29835  wlkp1lem8  29836  wwlks2onsym  30117  rusgrnumwwlks  30134  clwwlknclwwlkdifnum  30139  clwwlknonfin  30253  clwwlknonex2  30268  umgr3cyclex  30342  eupthp1  30375  eupth2eucrct  30376  frcond3  30428  frgr3v  30434  3vfriswmgr  30437  1to3vfriendship  30440  2pthfrgrrn  30441  3cyclfrgrrn1  30444  4cycl2v2nb  30448  frgrnbnb  30452  frgrncvvdeqlem3  30460  frgrncvvdeqlem6  30463  frgrhash2wsp  30491  fusgr2wsp2nb  30493  numclwwlk1  30520  avril1  30622  n0lplig  30643  hhph  31338  nonbooli  31811  pjss2i  31840  atssma  32538  isrrext  34258  hasheuni  34343  dmvlsiga  34387  measiuns  34475  eulerpartlemmf  34633  fissorduni  35346  fineqvrep  35371  onvf1odlem2  35408  onvf1odlem4  35410  cusgr3cyclex  35447  resconn  35557  cvmlift2lem9  35622  rdgprc0  36102  bj-snsetex  37409  bj-tagex  37433  bj-0int  37552  poimirlem30  38110  ftc1anclem3  38155  ftc1anclem6  38158  rrnheibor  38297  rngo1cl  38399  isdrngo1  38416  dfcoeleqvrels  39165  rnqmapeleldisjsim  39322  islpln2ah  40134  lhpocnel2  40604  cdlemg31b0N  41279  cdlemg31b0a  41280  cdlemh  41402  cdlemk19w  41557  aks4d1lem1  42640  sticksstones4  42727  mzpclval  43267  wopprc  43568  dfac21  43604  uniel  43755  sucomisnotcard  44081  binomcxplemdvsum  44892  binomcxp  44894  mccl  46135  fprodcn  46137  stoweidlem17  46552  fourierdlem89  46730  fourierdlem90  46731  fourierdlem91  46732  fourierdlem100  46741  omeiunltfirp  47054  hoidmvlelem5  47134  issmf  47263  issmff  47269  smflimlem4  47309  smflim  47312  smflim2  47341  smflimsuplem1  47355  smflimsuplem8  47362  smflimsup  47363  chnerlem1  47419  aiotaexb  47644  aiotavb  47645  aovvdm  47740  aovvfunressn  47742  aovrcl  47744  aovvoveq  47747  aov0nbovbi  47750  fnotaovb  47753  mod2addne  47925  prmdvdsfmtnof1lem1  48154  341fppr2  48317  9fppr8  48320  clnbupgrel  48417  grtriproplem  48522  grtrif1o  48525  grtriclwlk3  48528  usgrgrtrirex  48533  isubgr3stgrlem7  48555  grlimprclnbgr  48579  grlimprclnbgrvtx  48582  usgrexmpl1  48605  usgrexmpl2  48610  gpgvtxedg0  48646  gpgvtxedg1  48647  gpgedg2ov  48649  gpgedg2iv  48650  gpgprismgr4cycllem11  48688  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem2lem3  48699  pgnbgreunbgrlem2  48700  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5  48706  pgnbgreunbgr  48708  pgn4cyclex  48709  zlmodzxzldeplem3  49085  itscnhlinecirc02p  49368  fonex  49449  idemb  49741