Theorem eleq1i 2851

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 2848	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2144

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-cleq 2752  df-clel 2835

This theorem is used by:  eleq12i  2853  eqeltri  2856  eqneltri  2879  intexrab  5307  abssexg  5343  rmorabex  5427  otelxp  5694  xpsspw  5786  dfse2  6097  dfse3  6339  ordtri3or  6395  fressnfv  7165  fnotovb  7473  ovmpos  7569  abnex  7772  sucexb  7819  f1stres  8026  f2ndres  8027  elxp6  8036  ottpos  8257  dftpos4  8266  tfr2b  8408  tz7.48-3  8458  unfi  9190  fissorduni  9286  difinf  9307  fiint  9322  infssuni  9339  fsuppunbi  9385  r1pwALT  9864  djuexb  9994  alephprc  10182  fin1a2lem12  10493  axcclem  10539  zorn2lem4  10581  zornn0g  10587  grothomex  10918  grothprimlem  10922  addclprlem2  11106  axicn  11239  0mnnnnn0  12642  fcdmnn0fsupp  12668  pfxccatin12lem3  14886  pfxccat3  14888  swrdccat  14889  pfxccat3a  14892  swrdccat3blem  14893  swrdccat3b  14894  harmonic  16034  nprmi  16870  issubmgm  18897  issubm  19004  idresefmnd  19101  mulgfval  19285  oppgsubm  19582  idrespermg  19631  issrg  20420  srgfcl  20428  subrngrng  20808  opprsubrng  20817  rhmimasubrng  20824  cntzsubrng  20825  opprsubrg  20851  rngridlmcl  21502  isridlrng  21504  isridl  21551  resubdrg  21920  cpmidpmat  23197  kgencn  23881  kgencn2  23882  txdis1cn  23960  qtopres  24023  qtopcn  24039  cfinfil  24218  tgphaus  24442  xmeterval  24757  blval2  24887  metuel2  24890  iscvsp  25455  zclmncvs  25475  caucfil  25610  resscdrg  25685  finiunmbl  25871  iblre  26120  dvfsumlem2  26353  logno1  26970  rlimcnp2  27300  ppi2i  27502  gausslemma2dlem1a  27698  2lgslem4  27739  noxp1o  28026  usgrexmpl  29850  usgredgffibi  29911  nbupgrel  29932  nbuhgr2vtx1edgb  29939  nbusgreledg  29940  nbusgrf1o0  29956  nb3grpr  29969  nb3grpr2  29970  nb3gr2nb  29971  cusgrsizeinds  30039  cusgrfi  30045  finsumvtxdg2size  30137  wlkp1lem1  30258  wlkp1lem7  30264  wlkp1lem8  30265  wwlks2onsym  30555  rusgrnumwwlks  30572  clwwlknclwwlkdifnum  30577  clwwlknonfin  30691  clwwlknonex2  30706  umgr3cyclex  30790  eupthp1  30823  eupth2eucrct  30824  frcond3  30876  frgr3v  30882  3vfriswmgr  30885  1to3vfriendship  30888  2pthfrgrrn  30889  3cyclfrgrrn1  30892  4cycl2v2nb  30896  frgrnbnb  30900  frgrncvvdeqlem3  30908  frgrncvvdeqlem6  30911  frgrhash2wsp  30939  fusgr2wsp2nb  30941  numclwwlk1  30968  avril1  31070  n0lplig  31091  hhph  31786  nonbooli  32259  pjss2i  32288  atssma  32986  isrrext  34679  hasheuni  34764  dmvlsiga  34808  measiuns  34897  eulerpartlemmf  35054  rankse  35794  fineqvrep  35839  maxssj0  35946  onvf1odlem2  35952  onvf1odlem4  35954  cusgr3cyclex  35988  resconn  36098  cvmlift2lem9  36163  rdgprc0  36648  bj-snsetex  37969  bj-tagex  37993  bj-0int  38115  poimirlem30  38662  ftc1anclem3  38707  ftc1anclem6  38710  rrnheibor  38865  rngo1cl  38967  isdrngo1  38984  dfcoeleqvrels  39731  rnqmapeleldisjsim  39888  islpln2ah  40700  lhpocnel2  41170  cdlemg31b0N  41845  cdlemg31b0a  41846  cdlemh  41968  cdlemk19w  42123  aks4d1lem1  43206  sticksstones4  43293  mzpclval  43830  wopprc  44131  dfac21  44162  uniel  44313  sucomisnotcard  44639  binomcxplemdvsum  45433  binomcxp  45435  mccl  46704  fprodcn  46706  stoweidlem17  47121  fourierdlem89  47299  fourierdlem90  47300  fourierdlem91  47301  fourierdlem100  47310  omeiunltfirp  47623  hoidmvlelem5  47703  issmf  47832  issmff  47838  smflimlem4  47878  smflim  47881  smflim2  47910  smflimsuplem1  47924  smflimsuplem8  47931  smflimsup  47932  aiotaexb  48253  aiotavb  48254  aovvdm  48349  aovvfunressn  48351  aovrcl  48353  aovvoveq  48356  aov0nbovbi  48359  fnotaovb  48362  mod2addne  48534  prmdvdsfmtnof1lem1  48763  341fppr2  48926  9fppr8  48929  clnbupgrel  49026  grtriproplem  49131  grtrif1o  49134  grtriclwlk3  49137  usgrgrtrirex  49142  isubgr3stgrlem7  49164  grlimprclnbgr  49188  grlimprclnbgrvtx  49191  usgrexmpl1  49214  usgrexmpl2  49219  gpgvtxedg0  49255  gpgvtxedg1  49256  gpgedg2ov  49258  gpgedg2iv  49259  gpgprismgr4cycllem11  49297  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem2  49309  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5  49315  pgnbgreunbgr  49317  pgn4cyclex  49318  zlmodzxzldeplem3  49708  fonex  50072  idemb  50369  dvsec  51025  dvcsc  51026  dvcot  51027