Theorem eleq1i 2850

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

Syntax hints:   ↔ wb 198   = wceq 1507   ∈ wcel 2050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-ext 2744

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-cleq 2765  df-clel 2840

This theorem is referenced by:  eleq12i  2852  eqneltri  2853  eqeltri  2856  intexrab  5093  abssexg  5129  rmorabex  5203  xpsspw  5526  dfse2  5797  ordtri3or  6055  fressnfv  6739  fnotovb  7019  ovmpos  7108  abnex  7290  sucexb  7334  f1stres  7519  f2ndres  7520  elxp6  7529  ottpos  7699  dftpos4  7708  tfr2b  7830  tz7.48-3  7877  difinf  8577  fiint  8584  infssuni  8604  fsuppunbi  8643  r1pwALT  9063  djuexb  9126  alephprc  9313  fin1a2lem12  9625  axcclem  9671  zorn2lem4  9713  zornn0g  9719  grothomex  10043  grothprimlem  10047  addclprlem2  10231  axicn  10364  0mnnnnn0  11735  swrdccatin12lem3  13927  pfxccat3  13930  swrdccat3OLD  13931  swrdccat  13932  swrdccatOLD  13933  pfxccat3a  13936  swrdccat3blem  13938  swrdccat3b  13939  swrdccat3bOLD  13940  harmonic  15068  nprmi  15883  issubm  17809  mulgfval  18007  oppgsubm  18255  idrespermg  18294  issrg  18974  srgfcl  18982  opprsubrg  19273  resubdrg  20448  cpmidpmat  21179  kgencn  21862  kgencn2  21863  txdis1cn  21941  qtopres  22004  qtopcn  22020  cfinfil  22199  tgphaus  22422  xmeterval  22739  blval2  22869  metuel2  22872  iscvsp  23429  zclmncvs  23449  caucfil  23583  resscdrg  23658  finiunmbl  23842  iblre  24091  logno1  24914  rlimcnp2  25240  ppi2i  25442  gausslemma2dlem1a  25637  2lgslem4  25678  usgredgffibi  26803  nbupgrel  26824  nbuhgr2vtx1edgb  26831  nbusgreledg  26832  nbusgrf1o0  26848  nb3grpr  26861  nb3grpr2  26862  nb3gr2nb  26863  cusgrsizeinds  26931  cusgrfi  26937  finsumvtxdg2size  27029  wlkp1lem1  27155  wlkp1lem7  27161  wlkp1lem8  27162  wwlks2onsym  27458  rusgrnumwwlks  27474  rusgrnumwwlksOLD  27475  clwwlknclwwlkdifnum  27480  clwwlknonfin  27616  clwwlknonex2  27631  umgr3cyclex  27706  eupthp1  27740  eupth2eucrct  27741  frcond3  27797  frgr3v  27803  3vfriswmgr  27806  1to3vfriendship  27809  2pthfrgrrn  27810  3cyclfrgrrn1  27813  4cycl2v2nb  27817  frgrnbnb  27821  frgrncvvdeqlem3  27829  frgrncvvdeqlem6  27832  frgrhash2wsp  27860  fusgr2wsp2nb  27862  numclwwlk1  27903  avril1  28013  n0lplig  28031  hhph  28728  nonbooli  29203  pjss2i  29232  atssma  29930  isrrext  30885  hasheuni  30988  dmvlsiga  31033  measiuns  31121  eulerpartlemmf  31278  resconn  32078  cvmlift2lem9  32143  rdgprc0  32559  noxp1o  32691  bj-snsetex  33793  bj-tagex  33817  bj-0int  33903  poimirlem30  34363  ftc1anclem3  34410  ftc1anclem6  34413  rrnheibor  34557  rngo1cl  34659  isdrngo1  34676  dfcoeleqvrels  35301  islpln2ah  36130  lhpocnel2  36600  cdlemg31b0N  37275  cdlemg31b0a  37276  cdlemh  37398  cdlemk19w  37553  mzpclval  38717  wopprc  39023  dfac21  39062  binomcxplemdvsum  40103  binomcxp  40105  mccl  41310  fprodcn  41312  stoweidlem17  41733  fourierdlem89  41911  fourierdlem90  41912  fourierdlem91  41913  fourierdlem100  41922  omeiunltfirp  42232  hoidmvlelem5  42312  issmf  42436  issmff  42442  smflimlem4  42481  smflim  42484  smflim2  42511  smflimsuplem1  42525  smflimsuplem8  42532  smflimsup  42533  aiotaexb  42695  aiotavb  42696  aovvdm  42790  aovvfunressn  42792  aovrcl  42794  aovvoveq  42797  aov0nbovbi  42800  fnotaovb  42803  prmdvdsfmtnof1lem1  43114  341fppr2  43267  9fppr8  43270  issubmgm  43424  zlmodzxzldeplem3  43924  itscnhlinecirc02p  44140