Theorem eleq1i 2822

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2806

This theorem is referenced by:  eleq12i  2824  eqeltri  2827  eqneltri  2850  intexrab  5280  abssexg  5315  rmorabex  5395  otelxp  5655  xpsspw  5744  dfse2  6044  dfse3  6278  ordtri3or  6333  fressnfv  7088  fnotovb  7393  ovmpos  7489  abnex  7685  sucexb  7732  f1stres  7940  f2ndres  7941  elxp6  7950  ottpos  8161  dftpos4  8170  tfr2b  8310  tz7.48-3  8358  unfi  9075  difinf  9190  fiint  9206  infssuni  9225  fsuppunbi  9268  r1pwALT  9734  djuexb  9797  alephprc  9985  fin1a2lem12  10297  axcclem  10343  zorn2lem4  10385  zornn0g  10391  grothomex  10715  grothprimlem  10719  addclprlem2  10903  axicn  11036  0mnnnnn0  12408  fcdmnn0fsupp  12434  pfxccatin12lem3  14634  pfxccat3  14636  swrdccat  14637  pfxccat3a  14640  swrdccat3blem  14641  swrdccat3b  14642  harmonic  15761  nprmi  16595  issubmgm  18605  issubm  18706  idresefmnd  18802  mulgfval  18977  oppgsubm  19269  idrespermg  19318  issrg  20101  srgfcl  20109  subrngrng  20460  opprsubrng  20469  rhmimasubrng  20476  cntzsubrng  20477  opprsubrg  20503  rngridlmcl  21149  isridlrng  21151  isridl  21184  resubdrg  21540  cpmidpmat  22783  kgencn  23466  kgencn2  23467  txdis1cn  23545  qtopres  23608  qtopcn  23624  cfinfil  23803  tgphaus  24027  xmeterval  24342  blval2  24472  metuel2  24475  iscvsp  25050  zclmncvs  25070  caucfil  25205  resscdrg  25280  finiunmbl  25467  iblre  25717  dvfsumlem2  25955  logno1  26567  rlimcnp2  26898  ppi2i  27101  gausslemma2dlem1a  27298  2lgslem4  27339  noxp1o  27597  usgrexmpl  29236  usgredgffibi  29297  nbupgrel  29318  nbuhgr2vtx1edgb  29325  nbusgreledg  29326  nbusgrf1o0  29342  nb3grpr  29355  nb3grpr2  29356  nb3gr2nb  29357  cusgrsizeinds  29426  cusgrfi  29432  finsumvtxdg2size  29524  wlkp1lem1  29645  wlkp1lem7  29651  wlkp1lem8  29652  wwlks2onsym  29931  rusgrnumwwlks  29947  clwwlknclwwlkdifnum  29952  clwwlknonfin  30066  clwwlknonex2  30081  umgr3cyclex  30155  eupthp1  30188  eupth2eucrct  30189  frcond3  30241  frgr3v  30247  3vfriswmgr  30250  1to3vfriendship  30253  2pthfrgrrn  30254  3cyclfrgrrn1  30257  4cycl2v2nb  30261  frgrnbnb  30265  frgrncvvdeqlem3  30273  frgrncvvdeqlem6  30276  frgrhash2wsp  30304  fusgr2wsp2nb  30306  numclwwlk1  30333  avril1  30435  n0lplig  30455  hhph  31150  nonbooli  31623  pjss2i  31652  atssma  32350  isrrext  34005  hasheuni  34090  dmvlsiga  34134  measiuns  34222  eulerpartlemmf  34380  fissorduni  35093  fineqvrep  35129  onvf1odlem2  35140  onvf1odlem4  35142  cusgr3cyclex  35172  resconn  35282  cvmlift2lem9  35347  rdgprc0  35827  bj-snsetex  36997  bj-tagex  37021  bj-0int  37135  poimirlem30  37690  ftc1anclem3  37735  ftc1anclem6  37738  rrnheibor  37877  rngo1cl  37979  isdrngo1  37996  dfcoeleqvrels  38658  islpln2ah  39588  lhpocnel2  40058  cdlemg31b0N  40733  cdlemg31b0a  40734  cdlemh  40856  cdlemk19w  41011  aks4d1lem1  42095  sticksstones4  42182  mzpclval  42758  wopprc  43063  dfac21  43099  uniel  43250  sucomisnotcard  43577  binomcxplemdvsum  44388  binomcxp  44390  mccl  45638  fprodcn  45640  stoweidlem17  46055  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem100  46244  omeiunltfirp  46557  hoidmvlelem5  46637  issmf  46766  issmff  46772  smflimlem4  46812  smflim  46815  smflim2  46844  smflimsuplem1  46858  smflimsuplem8  46865  smflimsup  46866  aiotaexb  47120  aiotavb  47121  aovvdm  47216  aovvfunressn  47218  aovrcl  47220  aovvoveq  47223  aov0nbovbi  47226  fnotaovb  47229  mod2addne  47395  prmdvdsfmtnof1lem1  47615  341fppr2  47765  9fppr8  47768  clnbupgrel  47865  grtriproplem  47970  grtrif1o  47973  grtriclwlk3  47976  usgrgrtrirex  47981  isubgr3stgrlem7  48003  grlimprclnbgr  48027  grlimprclnbgrvtx  48030  usgrexmpl1  48053  usgrexmpl2  48058  gpgvtxedg0  48094  gpgvtxedg1  48095  gpgedg2ov  48097  gpgedg2iv  48098  gpgprismgr4cycllem11  48136  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem2  48148  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem5  48154  pgnbgreunbgr  48156  pgn4cyclex  48157  zlmodzxzldeplem3  48534  itscnhlinecirc02p  48817  fonex  48898  idemb  49191