Theorem eleq1i 2880

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

Syntax hints:   ↔ wb 209   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  eleq12i  2882  eqneltri  2883  eqeltri  2886  intexrab  5207  abssexg  5248  rmorabex  5317  xpsspw  5646  dfse2  5930  ordtri3or  6191  fressnfv  6899  fnotovb  7185  ovmpos  7277  abnex  7459  sucexb  7504  f1stres  7695  f2ndres  7696  elxp6  7705  ottpos  7885  dftpos4  7894  tfr2b  8015  tz7.48-3  8063  difinf  8772  fiint  8779  infssuni  8799  fsuppunbi  8838  r1pwALT  9259  djuexb  9322  alephprc  9510  fin1a2lem12  9822  axcclem  9868  zorn2lem4  9910  zornn0g  9916  grothomex  10240  grothprimlem  10244  addclprlem2  10428  axicn  10561  0mnnnnn0  11917  pfxccatin12lem3  14085  pfxccat3  14087  swrdccat  14088  pfxccat3a  14091  swrdccat3blem  14092  swrdccat3b  14093  harmonic  15206  nprmi  16023  issubm  17960  idresefmnd  18056  mulgfval  18218  oppgsubm  18482  idrespermg  18531  issrg  19250  srgfcl  19258  opprsubrg  19549  resubdrg  20297  cpmidpmat  21478  kgencn  22161  kgencn2  22162  txdis1cn  22240  qtopres  22303  qtopcn  22319  cfinfil  22498  tgphaus  22722  xmeterval  23039  blval2  23169  metuel2  23172  iscvsp  23733  zclmncvs  23753  caucfil  23887  resscdrg  23962  finiunmbl  24148  iblre  24397  logno1  25227  rlimcnp2  25552  ppi2i  25754  gausslemma2dlem1a  25949  2lgslem4  25990  usgredgffibi  27114  nbupgrel  27135  nbuhgr2vtx1edgb  27142  nbusgreledg  27143  nbusgrf1o0  27159  nb3grpr  27172  nb3grpr2  27173  nb3gr2nb  27174  cusgrsizeinds  27242  cusgrfi  27248  finsumvtxdg2size  27340  wlkp1lem1  27463  wlkp1lem7  27469  wlkp1lem8  27470  wwlks2onsym  27744  rusgrnumwwlks  27760  clwwlknclwwlkdifnum  27765  clwwlknonfin  27879  clwwlknonex2  27894  umgr3cyclex  27968  eupthp1  28001  eupth2eucrct  28002  frcond3  28054  frgr3v  28060  3vfriswmgr  28063  1to3vfriendship  28066  2pthfrgrrn  28067  3cyclfrgrrn1  28070  4cycl2v2nb  28074  frgrnbnb  28078  frgrncvvdeqlem3  28086  frgrncvvdeqlem6  28089  frgrhash2wsp  28117  fusgr2wsp2nb  28119  numclwwlk1  28146  avril1  28248  n0lplig  28266  hhph  28961  nonbooli  29434  pjss2i  29463  atssma  30161  isrrext  31351  hasheuni  31454  dmvlsiga  31498  measiuns  31586  eulerpartlemmf  31743  cusgr3cyclex  32496  resconn  32606  cvmlift2lem9  32671  rdgprc0  33151  noxp1o  33283  bj-snsetex  34399  bj-tagex  34423  bj-0int  34516  poimirlem30  35087  ftc1anclem3  35132  ftc1anclem6  35135  rrnheibor  35275  rngo1cl  35377  isdrngo1  35394  dfcoeleqvrels  36016  islpln2ah  36845  lhpocnel2  37315  cdlemg31b0N  37990  cdlemg31b0a  37991  cdlemh  38113  cdlemk19w  38268  3lexlogpow5ineq2  39342  mzpclval  39666  wopprc  39971  dfac21  40010  binomcxplemdvsum  41059  binomcxp  41061  mccl  42240  fprodcn  42242  stoweidlem17  42659  fourierdlem89  42837  fourierdlem90  42838  fourierdlem91  42839  fourierdlem100  42848  omeiunltfirp  43158  hoidmvlelem5  43238  issmf  43362  issmff  43368  smflimlem4  43407  smflim  43410  smflim2  43437  smflimsuplem1  43451  smflimsuplem8  43458  smflimsup  43459  aiotaexb  43646  aiotavb  43647  aovvdm  43741  aovvfunressn  43743  aovrcl  43745  aovvoveq  43748  aov0nbovbi  43751  fnotaovb  43754  prmdvdsfmtnof1lem1  44101  341fppr2  44252  9fppr8  44255  issubmgm  44409  zlmodzxzldeplem3  44911  itscnhlinecirc02p  45199