Theorem eleq1i 2816

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

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-clel 2802

This theorem is referenced by:  eleq12i  2818  eqeltri  2821  eqneltri  2844  intexrab  5343  abssexg  5382  rmorabex  5462  otelxp  5722  xpsspw  5811  dfse2  6105  dfse3  6344  ordtri3or  6403  fressnfv  7169  fnotovb  7470  ovmpos  7569  abnex  7760  sucexb  7808  f1stres  8018  f2ndres  8019  elxp6  8028  ottpos  8242  dftpos4  8251  tfr2b  8417  tz7.48-3  8465  unfi  9197  difinf  9342  fiint  9350  infssuni  9369  fsuppunbi  9414  r1pwALT  9871  djuexb  9934  alephprc  10124  fin1a2lem12  10436  axcclem  10482  zorn2lem4  10524  zornn0g  10530  grothomex  10854  grothprimlem  10858  addclprlem2  11042  axicn  11175  0mnnnnn0  12537  fcdmnn0fsupp  12562  pfxccatin12lem3  14718  pfxccat3  14720  swrdccat  14721  pfxccat3a  14724  swrdccat3blem  14725  swrdccat3b  14726  harmonic  15841  nprmi  16663  issubmgm  18665  issubm  18763  idresefmnd  18859  mulgfval  19033  oppgsubm  19328  idrespermg  19378  issrg  20140  srgfcl  20148  subrngrng  20499  opprsubrng  20508  rhmimasubrng  20515  cntzsubrng  20516  opprsubrg  20544  rngridlmcl  21125  isridlrng  21127  isridl  21159  resubdrg  21557  cpmidpmat  22819  kgencn  23504  kgencn2  23505  txdis1cn  23583  qtopres  23646  qtopcn  23662  cfinfil  23841  tgphaus  24065  xmeterval  24382  blval2  24515  metuel2  24518  iscvsp  25099  zclmncvs  25120  caucfil  25255  resscdrg  25330  finiunmbl  25517  iblre  25767  dvfsumlem2  26005  logno1  26615  rlimcnp2  26943  ppi2i  27146  gausslemma2dlem1a  27343  2lgslem4  27384  noxp1o  27642  usgredgffibi  29209  nbupgrel  29230  nbuhgr2vtx1edgb  29237  nbusgreledg  29238  nbusgrf1o0  29254  nb3grpr  29267  nb3grpr2  29268  nb3gr2nb  29269  cusgrsizeinds  29338  cusgrfi  29344  finsumvtxdg2size  29436  wlkp1lem1  29559  wlkp1lem7  29565  wlkp1lem8  29566  wwlks2onsym  29841  rusgrnumwwlks  29857  clwwlknclwwlkdifnum  29862  clwwlknonfin  29976  clwwlknonex2  29991  umgr3cyclex  30065  eupthp1  30098  eupth2eucrct  30099  frcond3  30151  frgr3v  30157  3vfriswmgr  30160  1to3vfriendship  30163  2pthfrgrrn  30164  3cyclfrgrrn1  30167  4cycl2v2nb  30171  frgrnbnb  30175  frgrncvvdeqlem3  30183  frgrncvvdeqlem6  30186  frgrhash2wsp  30214  fusgr2wsp2nb  30216  numclwwlk1  30243  avril1  30345  n0lplig  30365  hhph  31060  nonbooli  31533  pjss2i  31562  atssma  32260  isrrext  33732  hasheuni  33835  dmvlsiga  33879  measiuns  33967  eulerpartlemmf  34126  fineqvrep  34846  cusgr3cyclex  34877  resconn  34987  cvmlift2lem9  35052  rdgprc0  35520  bj-snsetex  36573  bj-tagex  36597  bj-0int  36711  poimirlem30  37254  ftc1anclem3  37299  ftc1anclem6  37302  rrnheibor  37441  rngo1cl  37543  isdrngo1  37560  dfcoeleqvrels  38223  islpln2ah  39152  lhpocnel2  39622  cdlemg31b0N  40297  cdlemg31b0a  40298  cdlemh  40420  cdlemk19w  40575  aks4d1lem1  41665  sticksstones4  41752  mzpclval  42287  wopprc  42593  dfac21  42632  uniel  42787  sucomisnotcard  43116  binomcxplemdvsum  43934  binomcxp  43936  mccl  45124  fprodcn  45126  stoweidlem17  45543  fourierdlem89  45721  fourierdlem90  45722  fourierdlem91  45723  fourierdlem100  45732  omeiunltfirp  46045  hoidmvlelem5  46125  issmf  46254  issmff  46260  smflimlem4  46300  smflim  46303  smflim2  46332  smflimsuplem1  46346  smflimsuplem8  46353  smflimsup  46354  aiotaexb  46607  aiotavb  46608  aovvdm  46703  aovvfunressn  46705  aovrcl  46707  aovvoveq  46710  aov0nbovbi  46713  fnotaovb  46716  prmdvdsfmtnof1lem1  47061  341fppr2  47211  9fppr8  47214  clnbupgrel  47310  zlmodzxzldeplem3  47756  itscnhlinecirc02p  48044