Theorem eleq1i 2692

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  eleq12i  2694  eqeltri  2697  intexrab  4823  abssexg  4851  rmorabex  4928  xpsspw  5233  dfse2  5499  ordtri3or  5755  fressnfv  6427  fnotovb  6694  ovmpt2s  6784  abnex  6965  snnexOLD  6967  sucexb  7009  iprc  7101  f1stres  7190  f2ndres  7191  elxp6  7200  ottpos  7362  dftpos4  7371  tfr2b  7492  tz7.48-3  7539  difinf  8230  fiint  8237  infssuni  8257  fsuppunbi  8296  r1pwALT  8709  alephprc  8922  fin1a2lem12  9233  axcclem  9279  zorn2lem4  9321  zornn0g  9327  grothomex  9651  grothprimlem  9655  addclprlem2  9839  axicn  9971  pnfnre  10081  mnfnre  10082  0mnnnnn0  11325  swrdccatin12lem3  13490  swrdccat3  13492  swrdccat  13493  swrdccat3blem  13495  swrdccat3b  13496  harmonic  14591  nprmi  15402  prmrec  15626  issubm  17347  oppgsubm  17792  idrespermg  17831  issrg  18507  srgfcl  18515  opprsubrg  18801  00lsp  18981  resubdrg  19954  cpmidpmat  20678  kgencn  21359  kgencn2  21360  txdis1cn  21438  qtopres  21501  qtopcn  21517  cfinfil  21697  tgphaus  21920  xmeterval  22237  blval2  22367  metuel2  22370  iscvsp  22928  zclmncvs  22948  caucfil  23081  resscdrg  23154  finiunmbl  23312  iblre  23560  logno1  24382  rlimcnp2  24693  ppi2i  24895  gausslemma2dlem1a  25090  2lgslem4  25131  usgredgffibi  26216  nbupgrel  26241  nbuhgr2vtx1edgb  26248  nbusgreledg  26249  nbusgrf1o0  26271  nb3grpr  26284  nb3grpr2  26285  nb3gr2nb  26286  cusgrsizeinds  26348  cusgrfi  26354  finsumvtxdg2size  26446  wlkp1lem1  26570  wlkp1lem7  26576  wlkp1lem8  26577  wwlks2onsym  26851  rusgrnumwwlks  26869  clwwlknclwwlkdifnum  26874  umgr3cyclex  27043  eupthp1  27076  eupth2eucrct  27077  frcond3  27133  frgr3v  27139  3vfriswmgr  27142  1to3vfriendship  27145  2pthfrgrrn  27146  3cyclfrgrrn1  27149  4cycl2v2nb  27153  frgrnbnb  27157  frgrncvvdeqlem3  27165  frgrncvvdeqlem6  27168  frgrhash2wsp  27196  fusgr2wsp2nb  27198  numclwwlkovf2exlem2  27212  numclwwlkffin  27214  avril1  27319  n0lplig  27335  hhph  28035  nonbooli  28510  pjss2i  28539  atssma  29237  isrrext  30044  hasheuni  30147  dmvlsiga  30192  measiuns  30280  eulerpartlemmf  30437  resconn  31228  cvmlift2lem9  31293  rdgprc0  31699  noxp1o  31816  bj-snsetex  32951  bj-tagex  32975  bj-0int  33055  bj-pinftynrr  33109  bj-minftynrr  33113  poimirlem30  33439  ftc1anclem3  33487  ftc1anclem6  33490  rrnheibor  33636  rngo1cl  33738  isdrngo1  33755  islpln2ah  34835  lhpocnel2  35305  cdlemg31b0N  35982  cdlemg31b0a  35983  cdlemh  36105  cdlemk19w  36260  mzpclval  37288  wopprc  37597  dfac21  37636  binomcxplemdvsum  38554  binomcxp  38556  eqneltri  39246  mccl  39830  fprodcn  39832  stoweidlem17  40234  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem100  40423  omeiunltfirp  40733  hoidmvlelem5  40813  issmf  40937  issmff  40943  smflimlem4  40982  smflim  40985  smflim2  41012  smflimsuplem1  41026  smflimsuplem8  41033  smflimsup  41034  aovvdm  41265  aovvfunressn  41267  aovrcl  41269  aovvoveq  41272  aov0nbovbi  41275  fnotaovb  41278  pfxccat3  41426  pfxccat3a  41429  prmdvdsfmtnof1lem1  41496  issubmgm  41789  zlmodzxzldeplem3  42291