Theorem eleq1i 2855

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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

This theorem is used by:  eleq12i  2857  eqeltri  2860  eqneltri  2883  intexrab  5315  abssexg  5351  rmorabex  5435  otelxp  5702  xpsspw  5796  dfse2  6116  dfse3  6365  ordtri3or  6421  fressnfv  7196  fnotovb  7503  ovmpos  7600  abnex  7803  sucexb  7852  f1stres  8059  f2ndres  8060  elxp6  8069  ottpos  8291  dftpos4  8300  tfr2b  8442  tz7.48-3  8492  unfi  9224  fissorduni  9320  difinf  9341  fiint  9356  infssuni  9373  fsuppunbi  9418  r1pwALT  9897  djuexb  10027  alephprc  10217  fin1a2lem12  10528  axcclem  10574  zorn2lem4  10616  zornn0g  10622  grothomex  10953  grothprimlem  10957  addclprlem2  11141  axicn  11274  0mnnnnn0  12678  fcdmnn0fsupp  12704  pfxccatin12lem3  14923  pfxccat3  14925  swrdccat  14926  pfxccat3a  14929  swrdccat3blem  14930  swrdccat3b  14931  harmonic  16072  nprmi  16908  issubmgm  18941  issubm  19048  idresefmnd  19145  mulgfval  19329  oppgsubm  19627  idrespermg  19676  issrg  20465  srgfcl  20473  subrngrng  20853  opprsubrng  20862  rhmimasubrng  20869  cntzsubrng  20870  opprsubrg  20896  rngridlmcl  21547  isridlrng  21549  isridl  21596  resubdrg  21969  cpmidpmat  23246  kgencn  23930  kgencn2  23931  txdis1cn  24009  qtopres  24072  qtopcn  24088  cfinfil  24267  tgphaus  24491  xmeterval  24806  blval2  24936  metuel2  24939  iscvsp  25504  zclmncvs  25524  caucfil  25659  resscdrg  25734  finiunmbl  25920  iblre  26169  dvfsumlem2  26402  logno1  27021  rlimcnp2  27351  ppi2i  27553  gausslemma2dlem1a  27749  2lgslem4  27790  noxp1o  28077  usgrexmpl  29901  usgredgffibi  29962  nbupgrel  29983  nbuhgr2vtx1edgb  29990  nbusgreledg  29991  nbusgrf1o0  30007  nb3grpr  30020  nb3grpr2  30021  nb3gr2nb  30022  cusgrsizeinds  30090  cusgrfi  30096  finsumvtxdg2size  30188  wlkp1lem1  30309  wlkp1lem7  30315  wlkp1lem8  30316  wwlks2onsym  30606  rusgrnumwwlks  30623  clwwlknclwwlkdifnum  30628  clwwlknonfin  30742  clwwlknonex2  30757  umgr3cyclex  30841  eupthp1  30874  eupth2eucrct  30875  frcond3  30927  frgr3v  30933  3vfriswmgr  30936  1to3vfriendship  30939  2pthfrgrrn  30940  3cyclfrgrrn1  30943  4cycl2v2nb  30947  frgrnbnb  30951  frgrncvvdeqlem3  30959  frgrncvvdeqlem6  30962  frgrhash2wsp  30990  fusgr2wsp2nb  30992  numclwwlk1  31019  avril1  31121  n0lplig  31142  hhph  31837  nonbooli  32310  pjss2i  32339  atssma  33037  isrrext  34743  hasheuni  34828  dmvlsiga  34872  measiuns  34961  eulerpartlemmf  35118  rankse  35864  fineqvrep  35923  maxssj0  36047  onvf1odlem2  36073  onvf1odlem4  36075  cusgr3cyclex  36109  resconn  36219  cvmlift2lem9  36284  rdgprc0  36770  bj-snsetex  38091  bj-tagex  38115  bj-0int  38292  poimirlem30  38836  ftc1anclem3  38881  ftc1anclem6  38884  rrnheibor  39037  rngo1cl  39139  isdrngo1  39156  dfcoeleqvrels  39903  rnqmapeleldisjsim  40060  islpln2ah  40872  lhpocnel2  41342  cdlemg31b0N  42017  cdlemg31b0a  42018  cdlemh  42140  cdlemk19w  42295  aks4d1lem1  43378  sticksstones4  43465  mzpclval  44002  wopprc  44303  dfac21  44334  uniel  44480  sucomisnotcard  44806  binomcxplemdvsum  45600  binomcxp  45602  mccl  46883  fprodcn  46885  stoweidlem17  47300  fourierdlem89  47478  fourierdlem90  47479  fourierdlem91  47480  fourierdlem100  47489  omeiunltfirp  47802  hoidmvlelem5  47882  issmf  48011  issmff  48017  smflimlem4  48057  smflim  48060  smflim2  48089  smflimsuplem1  48103  smflimsuplem8  48110  smflimsup  48111  aiotaexb  48432  aiotavb  48433  aovvdm  48528  aovvfunressn  48530  aovrcl  48532  aovvoveq  48535  aov0nbovbi  48538  fnotaovb  48541  mod2addne  48713  prmdvdsfmtnof1lem1  48942  341fppr2  49105  9fppr8  49108  clnbupgrel  49205  grtriproplem  49310  grtrif1o  49313  grtriclwlk3  49316  usgrgrtrirex  49321  isubgr3stgrlem7  49343  grlimprclnbgr  49367  grlimprclnbgrvtx  49370  usgrexmpl1  49393  usgrexmpl2  49398  gpgvtxedg0  49434  gpgvtxedg1  49435  gpgedg2ov  49437  gpgedg2iv  49438  gpgprismgr4cycllem11  49476  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem2  49488  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5  49494  pgnbgreunbgr  49496  pgn4cyclex  49497  zlmodzxzldeplem3  49945  fonex  50309  idemb  50606  dvsec  51284  dvcsc  51285  dvcot  51286