Theorem eleq1i 2883

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

Syntax hints:   ↔ wb 197   = wceq 1637   ∈ wcel 2157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2806  df-clel 2809

This theorem is referenced by:  eleq12i  2885  eqeltri  2888  intexrab  5022  abssexg  5058  rmorabex  5125  xpsspw  5441  dfse2  5716  ordtri3or  5975  fressnfv  6654  fnotovb  6926  fnotovbOLD  6927  ovmpt2s  7017  abnex  7198  snnexOLD  7200  sucexb  7242  iprc  7334  f1stres  7425  f2ndres  7426  elxp6  7435  ottpos  7600  dftpos4  7609  tfr2b  7731  tz7.48-3  7778  difinf  8472  fiint  8479  infssuni  8499  fsuppunbi  8538  r1pwALT  8959  alephprc  9208  fin1a2lem12  9521  axcclem  9567  zorn2lem4  9609  zornn0g  9615  grothomex  9939  grothprimlem  9943  addclprlem2  10127  axicn  10259  pnfnre  10369  mnfnre  10370  0mnnnnn0  11594  swrdccatin12lem3  13717  swrdccat3  13719  swrdccat  13720  swrdccat3blem  13722  swrdccat3b  13723  harmonic  14816  nprmi  15623  prmrec  15846  issubm  17555  oppgsubm  17996  idrespermg  18035  issrg  18712  srgfcl  18720  opprsubrg  19008  00lsp  19191  resubdrg  20166  cpmidpmat  20895  kgencn  21577  kgencn2  21578  txdis1cn  21656  qtopres  21719  qtopcn  21735  cfinfil  21914  tgphaus  22137  xmeterval  22454  blval2  22584  metuel2  22587  iscvsp  23144  zclmncvs  23164  caucfil  23298  resscdrg  23371  finiunmbl  23531  iblre  23780  logno1  24602  rlimcnp2  24913  ppi2i  25115  gausslemma2dlem1a  25310  2lgslem4  25351  usgredgffibi  26438  nbupgrel  26463  nbuhgr2vtx1edgb  26470  nbusgreledg  26471  nbusgrf1o0  26493  nb3grpr  26506  nb3grpr2  26507  nb3gr2nb  26508  cusgrsizeinds  26582  cusgrfi  26588  finsumvtxdg2size  26680  wlkp1lem1  26804  wlkp1lem7  26810  wlkp1lem8  26811  wwlks2onsym  27105  rusgrnumwwlks  27122  clwwlknclwwlkdifnum  27127  clwwlknclwwlkdifnumOLD  27129  clwwlknonfin  27267  clwwlknonex2  27284  umgr3cyclex  27362  eupthp1  27395  eupth2eucrct  27396  frcond3  27450  frgr3v  27456  3vfriswmgr  27459  1to3vfriendship  27462  2pthfrgrrn  27463  3cyclfrgrrn1  27466  4cycl2v2nb  27470  frgrnbnb  27474  frgrncvvdeqlem3  27482  frgrncvvdeqlem6  27485  frgrhash2wsp  27513  fusgr2wsp2nb  27515  numclwwlk1  27547  avril1  27656  n0lplig  27672  hhph  28369  nonbooli  28844  pjss2i  28873  atssma  29571  isrrext  30375  hasheuni  30478  dmvlsiga  30523  measiuns  30611  eulerpartlemmf  30768  resconn  31556  cvmlift2lem9  31621  rdgprc0  32024  noxp1o  32142  bj-snsetex  33263  bj-tagex  33287  bj-0int  33368  bj-pinftynrr  33428  bj-minftynrr  33432  poimirlem30  33754  ftc1anclem3  33801  ftc1anclem6  33804  rrnheibor  33949  rngo1cl  34051  isdrngo1  34068  islpln2ah  35331  lhpocnel2  35801  cdlemg31b0N  36476  cdlemg31b0a  36477  cdlemh  36599  cdlemk19w  36754  mzpclval  37791  wopprc  38099  dfac21  38138  binomcxplemdvsum  39055  binomcxp  39057  eqneltri  39740  mccl  40311  fprodcn  40313  stoweidlem17  40714  fourierdlem89  40892  fourierdlem90  40893  fourierdlem91  40894  fourierdlem100  40903  omeiunltfirp  41216  hoidmvlelem5  41296  issmf  41420  issmff  41426  smflimlem4  41465  smflim  41468  smflim2  41495  smflimsuplem1  41509  smflimsuplem8  41516  smflimsup  41517  aiotaexb  41674  aiotavb  41675  aovvdm  41775  aovvfunressn  41777  aovrcl  41779  aovvoveq  41782  aov0nbovbi  41785  fnotaovb  41788  pfxccat3  42002  pfxccat3a  42005  prmdvdsfmtnof1lem1  42072  issubmgm  42358  zlmodzxzldeplem3  42860