Theorem eleq1i 2903

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 2900	. 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 2793

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

This theorem is referenced by:  eleq12i  2905  eqneltri  2906  eqeltri  2909  intexrab  5243  abssexg  5283  rmorabex  5352  xpsspw  5682  dfse2  5963  ordtri3or  6223  fressnfv  6922  fnotovb  7206  ovmpos  7298  abnex  7479  sucexb  7524  f1stres  7713  f2ndres  7714  elxp6  7723  ottpos  7902  dftpos4  7911  tfr2b  8032  tz7.48-3  8080  difinf  8788  fiint  8795  infssuni  8815  fsuppunbi  8854  r1pwALT  9275  djuexb  9338  alephprc  9525  fin1a2lem12  9833  axcclem  9879  zorn2lem4  9921  zornn0g  9927  grothomex  10251  grothprimlem  10255  addclprlem2  10439  axicn  10572  0mnnnnn0  11930  pfxccatin12lem3  14094  pfxccat3  14096  swrdccat  14097  pfxccat3a  14100  swrdccat3blem  14101  swrdccat3b  14102  harmonic  15214  nprmi  16033  issubm  17968  idresefmnd  18064  mulgfval  18226  oppgsubm  18490  idrespermg  18539  issrg  19257  srgfcl  19265  opprsubrg  19556  resubdrg  20752  cpmidpmat  21481  kgencn  22164  kgencn2  22165  txdis1cn  22243  qtopres  22306  qtopcn  22322  cfinfil  22501  tgphaus  22725  xmeterval  23042  blval2  23172  metuel2  23175  iscvsp  23732  zclmncvs  23752  caucfil  23886  resscdrg  23961  finiunmbl  24145  iblre  24394  logno1  25219  rlimcnp2  25544  ppi2i  25746  gausslemma2dlem1a  25941  2lgslem4  25982  usgredgffibi  27106  nbupgrel  27127  nbuhgr2vtx1edgb  27134  nbusgreledg  27135  nbusgrf1o0  27151  nb3grpr  27164  nb3grpr2  27165  nb3gr2nb  27166  cusgrsizeinds  27234  cusgrfi  27240  finsumvtxdg2size  27332  wlkp1lem1  27455  wlkp1lem7  27461  wlkp1lem8  27462  wwlks2onsym  27737  rusgrnumwwlks  27753  clwwlknclwwlkdifnum  27758  clwwlknonfin  27873  clwwlknonex2  27888  umgr3cyclex  27962  eupthp1  27995  eupth2eucrct  27996  frcond3  28048  frgr3v  28054  3vfriswmgr  28057  1to3vfriendship  28060  2pthfrgrrn  28061  3cyclfrgrrn1  28064  4cycl2v2nb  28068  frgrnbnb  28072  frgrncvvdeqlem3  28080  frgrncvvdeqlem6  28083  frgrhash2wsp  28111  fusgr2wsp2nb  28113  numclwwlk1  28140  avril1  28242  n0lplig  28260  hhph  28955  nonbooli  29428  pjss2i  29457  atssma  30155  isrrext  31241  hasheuni  31344  dmvlsiga  31388  measiuns  31476  eulerpartlemmf  31633  cusgr3cyclex  32383  resconn  32493  cvmlift2lem9  32558  rdgprc0  33038  noxp1o  33170  bj-snsetex  34278  bj-tagex  34302  bj-0int  34396  poimirlem30  34937  ftc1anclem3  34984  ftc1anclem6  34987  rrnheibor  35130  rngo1cl  35232  isdrngo1  35249  dfcoeleqvrels  35871  islpln2ah  36700  lhpocnel2  37170  cdlemg31b0N  37845  cdlemg31b0a  37846  cdlemh  37968  cdlemk19w  38123  mzpclval  39371  wopprc  39676  dfac21  39715  binomcxplemdvsum  40736  binomcxp  40738  mccl  41928  fprodcn  41930  stoweidlem17  42351  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem100  42540  omeiunltfirp  42850  hoidmvlelem5  42930  issmf  43054  issmff  43060  smflimlem4  43099  smflim  43102  smflim2  43129  smflimsuplem1  43143  smflimsuplem8  43150  smflimsup  43151  aiotaexb  43338  aiotavb  43339  aovvdm  43433  aovvfunressn  43435  aovrcl  43437  aovvoveq  43440  aov0nbovbi  43443  fnotaovb  43446  prmdvdsfmtnof1lem1  43795  341fppr2  43948  9fppr8  43951  issubmgm  44105  zlmodzxzldeplem3  44606  itscnhlinecirc02p  44821