Theorem eleq1i 2824

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-clel 2810

This theorem is referenced by:  eleq12i  2826  eqeltri  2829  eqneltri  2852  intexrab  5340  abssexg  5380  rmorabex  5460  otelxp  5720  xpsspw  5809  dfse2  6099  dfse3  6337  ordtri3or  6396  fressnfv  7160  fnotovb  7461  ovmpos  7558  abnex  7746  sucexb  7794  f1stres  8001  f2ndres  8002  elxp6  8011  ottpos  8223  dftpos4  8232  tfr2b  8398  tz7.48-3  8446  unfi  9174  difinf  9318  fiint  9326  infssuni  9345  fsuppunbi  9386  r1pwALT  9843  djuexb  9906  alephprc  10096  fin1a2lem12  10408  axcclem  10454  zorn2lem4  10496  zornn0g  10502  grothomex  10826  grothprimlem  10830  addclprlem2  11014  axicn  11147  0mnnnnn0  12508  fcdmnn0fsupp  12533  pfxccatin12lem3  14686  pfxccat3  14688  swrdccat  14689  pfxccat3a  14692  swrdccat3blem  14693  swrdccat3b  14694  harmonic  15809  nprmi  16630  issubmgm  18627  issubm  18720  idresefmnd  18816  mulgfval  18988  oppgsubm  19270  idrespermg  19320  issrg  20082  srgfcl  20090  subrngrng  20438  opprsubrng  20447  rhmimasubrng  20454  cntzsubrng  20455  opprsubrg  20483  rngridlmcl  20983  isridl  21008  isridlrng  21031  resubdrg  21380  cpmidpmat  22595  kgencn  23280  kgencn2  23281  txdis1cn  23359  qtopres  23422  qtopcn  23438  cfinfil  23617  tgphaus  23841  xmeterval  24158  blval2  24291  metuel2  24294  iscvsp  24868  zclmncvs  24889  caucfil  25024  resscdrg  25099  finiunmbl  25285  iblre  25535  logno1  26368  rlimcnp2  26695  ppi2i  26897  gausslemma2dlem1a  27092  2lgslem4  27133  noxp1o  27390  usgredgffibi  28836  nbupgrel  28857  nbuhgr2vtx1edgb  28864  nbusgreledg  28865  nbusgrf1o0  28881  nb3grpr  28894  nb3grpr2  28895  nb3gr2nb  28896  cusgrsizeinds  28964  cusgrfi  28970  finsumvtxdg2size  29062  wlkp1lem1  29185  wlkp1lem7  29191  wlkp1lem8  29192  wwlks2onsym  29467  rusgrnumwwlks  29483  clwwlknclwwlkdifnum  29488  clwwlknonfin  29602  clwwlknonex2  29617  umgr3cyclex  29691  eupthp1  29724  eupth2eucrct  29725  frcond3  29777  frgr3v  29783  3vfriswmgr  29786  1to3vfriendship  29789  2pthfrgrrn  29790  3cyclfrgrrn1  29793  4cycl2v2nb  29797  frgrnbnb  29801  frgrncvvdeqlem3  29809  frgrncvvdeqlem6  29812  frgrhash2wsp  29840  fusgr2wsp2nb  29842  numclwwlk1  29869  avril1  29971  n0lplig  29991  hhph  30686  nonbooli  31159  pjss2i  31188  atssma  31886  isrrext  33266  hasheuni  33369  dmvlsiga  33413  measiuns  33501  eulerpartlemmf  33660  fineqvrep  34381  cusgr3cyclex  34413  resconn  34523  cvmlift2lem9  34588  rdgprc0  35057  gg-dvfsumlem2  35469  bj-snsetex  36147  bj-tagex  36171  bj-0int  36285  poimirlem30  36821  ftc1anclem3  36866  ftc1anclem6  36869  rrnheibor  37008  rngo1cl  37110  isdrngo1  37127  dfcoeleqvrels  37794  islpln2ah  38723  lhpocnel2  39193  cdlemg31b0N  39868  cdlemg31b0a  39869  cdlemh  39991  cdlemk19w  40146  aks4d1lem1  41233  sticksstones4  41271  mzpclval  41765  wopprc  42071  dfac21  42110  uniel  42268  sucomisnotcard  42597  binomcxplemdvsum  43416  binomcxp  43418  mccl  44613  fprodcn  44615  stoweidlem17  45032  fourierdlem89  45210  fourierdlem90  45211  fourierdlem91  45212  fourierdlem100  45221  omeiunltfirp  45534  hoidmvlelem5  45614  issmf  45743  issmff  45749  smflimlem4  45789  smflim  45792  smflim2  45821  smflimsuplem1  45835  smflimsuplem8  45842  smflimsup  45843  aiotaexb  46096  aiotavb  46097  aovvdm  46192  aovvfunressn  46194  aovrcl  46196  aovvoveq  46199  aov0nbovbi  46202  fnotaovb  46205  prmdvdsfmtnof1lem1  46551  341fppr2  46701  9fppr8  46704  zlmodzxzldeplem3  47271  itscnhlinecirc02p  47559