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 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-clel 2836

This theorem is used by:  eleq12i  2854  eqeltri  2857  eqneltri  2880  intexrab  5308  abssexg  5344  rmorabex  5428  otelxp  5695  xpsspw  5787  dfse2  6098  dfse3  6338  ordtri3or  6394  fressnfv  7162  fnotovb  7470  ovmpos  7566  abnex  7769  sucexb  7816  f1stres  8023  f2ndres  8024  elxp6  8033  ottpos  8246  dftpos4  8255  tfr2b  8397  tz7.48-3  8447  unfi  9179  fissorduni  9275  difinf  9296  fiint  9311  infssuni  9328  fsuppunbi  9374  r1pwALT  9853  djuexb  9983  alephprc  10171  fin1a2lem12  10482  axcclem  10528  zorn2lem4  10570  zornn0g  10576  grothomex  10907  grothprimlem  10911  addclprlem2  11095  axicn  11228  0mnnnnn0  12631  fcdmnn0fsupp  12657  pfxccatin12lem3  14874  pfxccat3  14876  swrdccat  14877  pfxccat3a  14880  swrdccat3blem  14881  swrdccat3b  14882  harmonic  16021  nprmi  16857  issubmgm  18884  issubm  18991  idresefmnd  19088  mulgfval  19272  oppgsubm  19569  idrespermg  19618  issrg  20407  srgfcl  20415  subrngrng  20795  opprsubrng  20804  rhmimasubrng  20811  cntzsubrng  20812  opprsubrg  20838  rngridlmcl  21489  isridlrng  21491  isridl  21538  resubdrg  21907  cpmidpmat  23184  kgencn  23868  kgencn2  23869  txdis1cn  23947  qtopres  24010  qtopcn  24026  cfinfil  24205  tgphaus  24429  xmeterval  24744  blval2  24874  metuel2  24877  iscvsp  25442  zclmncvs  25462  caucfil  25597  resscdrg  25672  finiunmbl  25858  iblre  26107  dvfsumlem2  26340  logno1  26957  rlimcnp2  27287  ppi2i  27489  gausslemma2dlem1a  27685  2lgslem4  27726  noxp1o  28013  usgrexmpl  29837  usgredgffibi  29898  nbupgrel  29919  nbuhgr2vtx1edgb  29926  nbusgreledg  29927  nbusgrf1o0  29943  nb3grpr  29956  nb3grpr2  29957  nb3gr2nb  29958  cusgrsizeinds  30026  cusgrfi  30032  finsumvtxdg2size  30124  wlkp1lem1  30245  wlkp1lem7  30251  wlkp1lem8  30252  wwlks2onsym  30542  rusgrnumwwlks  30559  clwwlknclwwlkdifnum  30564  clwwlknonfin  30678  clwwlknonex2  30693  umgr3cyclex  30777  eupthp1  30810  eupth2eucrct  30811  frcond3  30863  frgr3v  30869  3vfriswmgr  30872  1to3vfriendship  30875  2pthfrgrrn  30876  3cyclfrgrrn1  30879  4cycl2v2nb  30883  frgrnbnb  30887  frgrncvvdeqlem3  30895  frgrncvvdeqlem6  30898  frgrhash2wsp  30926  fusgr2wsp2nb  30928  numclwwlk1  30955  avril1  31057  n0lplig  31078  hhph  31773  nonbooli  32246  pjss2i  32275  atssma  32973  isrrext  34625  hasheuni  34710  dmvlsiga  34754  measiuns  34843  eulerpartlemmf  35000  fineqvrep  35765  onvf1odlem2  35866  onvf1odlem4  35868  cusgr3cyclex  35890  resconn  35990  cvmlift2lem9  36055  rdgprc0  36535  bj-snsetex  37856  bj-tagex  37880  bj-0int  38002  poimirlem30  38548  ftc1anclem3  38593  ftc1anclem6  38596  rrnheibor  38751  rngo1cl  38853  isdrngo1  38870  dfcoeleqvrels  39617  rnqmapeleldisjsim  39774  islpln2ah  40586  lhpocnel2  41056  cdlemg31b0N  41731  cdlemg31b0a  41732  cdlemh  41854  cdlemk19w  42009  aks4d1lem1  43092  sticksstones4  43179  mzpclval  43715  wopprc  44016  dfac21  44052  uniel  44203  sucomisnotcard  44529  binomcxplemdvsum  45324  binomcxp  45326  mccl  46579  fprodcn  46581  stoweidlem17  46996  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem100  47185  omeiunltfirp  47498  hoidmvlelem5  47578  issmf  47707  issmff  47713  smflimlem4  47753  smflim  47756  smflim2  47785  smflimsuplem1  47799  smflimsuplem8  47806  smflimsup  47807  aiotaexb  48128  aiotavb  48129  aovvdm  48224  aovvfunressn  48226  aovrcl  48228  aovvoveq  48231  aov0nbovbi  48234  fnotaovb  48237  mod2addne  48409  prmdvdsfmtnof1lem1  48638  341fppr2  48801  9fppr8  48804  clnbupgrel  48901  grtriproplem  49006  grtrif1o  49009  grtriclwlk3  49012  usgrgrtrirex  49017  isubgr3stgrlem7  49039  grlimprclnbgr  49063  grlimprclnbgrvtx  49066  usgrexmpl1  49089  usgrexmpl2  49094  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedg2ov  49133  gpgedg2iv  49134  gpgprismgr4cycllem11  49172  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5  49190  pgnbgreunbgr  49192  pgn4cyclex  49193  zlmodzxzldeplem3  49583  itscnhlinecirc02p  49866  fonex  49946  idemb  50236  dvsec  50825  dvcsc  50826  dvcot  50827