Theorem eleq1i 2905

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-clel 2895

This theorem is referenced by:  eleq12i  2907  eqneltri  2908  eqeltri  2911  intexrab  5245  abssexg  5285  rmorabex  5354  xpsspw  5684  dfse2  5965  ordtri3or  6225  fressnfv  6924  fnotovb  7208  ovmpos  7300  abnex  7481  sucexb  7526  f1stres  7715  f2ndres  7716  elxp6  7725  ottpos  7904  dftpos4  7913  tfr2b  8034  tz7.48-3  8082  difinf  8790  fiint  8797  infssuni  8817  fsuppunbi  8856  r1pwALT  9277  djuexb  9340  alephprc  9527  fin1a2lem12  9835  axcclem  9881  zorn2lem4  9923  zornn0g  9929  grothomex  10253  grothprimlem  10257  addclprlem2  10441  axicn  10574  0mnnnnn0  11932  pfxccatin12lem3  14096  pfxccat3  14098  swrdccat  14099  pfxccat3a  14102  swrdccat3blem  14103  swrdccat3b  14104  harmonic  15216  nprmi  16035  issubm  17970  idresefmnd  18066  mulgfval  18228  oppgsubm  18492  idrespermg  18541  issrg  19259  srgfcl  19267  opprsubrg  19558  resubdrg  20754  cpmidpmat  21483  kgencn  22166  kgencn2  22167  txdis1cn  22245  qtopres  22308  qtopcn  22324  cfinfil  22503  tgphaus  22727  xmeterval  23044  blval2  23174  metuel2  23177  iscvsp  23734  zclmncvs  23754  caucfil  23888  resscdrg  23963  finiunmbl  24147  iblre  24396  logno1  25221  rlimcnp2  25546  ppi2i  25748  gausslemma2dlem1a  25943  2lgslem4  25984  usgredgffibi  27108  nbupgrel  27129  nbuhgr2vtx1edgb  27136  nbusgreledg  27137  nbusgrf1o0  27153  nb3grpr  27166  nb3grpr2  27167  nb3gr2nb  27168  cusgrsizeinds  27236  cusgrfi  27242  finsumvtxdg2size  27334  wlkp1lem1  27457  wlkp1lem7  27463  wlkp1lem8  27464  wwlks2onsym  27739  rusgrnumwwlks  27755  clwwlknclwwlkdifnum  27760  clwwlknonfin  27875  clwwlknonex2  27890  umgr3cyclex  27964  eupthp1  27997  eupth2eucrct  27998  frcond3  28050  frgr3v  28056  3vfriswmgr  28059  1to3vfriendship  28062  2pthfrgrrn  28063  3cyclfrgrrn1  28066  4cycl2v2nb  28070  frgrnbnb  28074  frgrncvvdeqlem3  28082  frgrncvvdeqlem6  28085  frgrhash2wsp  28113  fusgr2wsp2nb  28115  numclwwlk1  28142  avril1  28244  n0lplig  28262  hhph  28957  nonbooli  29430  pjss2i  29459  atssma  30157  isrrext  31243  hasheuni  31346  dmvlsiga  31390  measiuns  31478  eulerpartlemmf  31635  cusgr3cyclex  32385  resconn  32495  cvmlift2lem9  32560  rdgprc0  33040  noxp1o  33172  bj-snsetex  34277  bj-tagex  34301  bj-0int  34395  poimirlem30  34924  ftc1anclem3  34971  ftc1anclem6  34974  rrnheibor  35117  rngo1cl  35219  isdrngo1  35236  dfcoeleqvrels  35858  islpln2ah  36687  lhpocnel2  37157  cdlemg31b0N  37832  cdlemg31b0a  37833  cdlemh  37955  cdlemk19w  38110  mzpclval  39329  wopprc  39634  dfac21  39673  binomcxplemdvsum  40694  binomcxp  40696  mccl  41886  fprodcn  41888  stoweidlem17  42309  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem100  42498  omeiunltfirp  42808  hoidmvlelem5  42888  issmf  43012  issmff  43018  smflimlem4  43057  smflim  43060  smflim2  43087  smflimsuplem1  43101  smflimsuplem8  43108  smflimsup  43109  aiotaexb  43296  aiotavb  43297  aovvdm  43391  aovvfunressn  43393  aovrcl  43395  aovvoveq  43398  aov0nbovbi  43401  fnotaovb  43404  prmdvdsfmtnof1lem1  43753  341fppr2  43906  9fppr8  43909  issubmgm  44063  zlmodzxzldeplem3  44564  itscnhlinecirc02p  44779