Theorem eleq1i 2823

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 2820	. 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 2702

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

This theorem is referenced by:  eleq12i  2825  eqeltri  2828  eqneltri  2851  intexrab  5302  abssexg  5342  rmorabex  5422  otelxp  5681  xpsspw  5770  dfse2  6057  dfse3  6295  ordtri3or  6354  fressnfv  7111  fnotovb  7412  ovmpos  7508  abnex  7696  sucexb  7744  f1stres  7950  f2ndres  7951  elxp6  7960  ottpos  8172  dftpos4  8181  tfr2b  8347  tz7.48-3  8395  unfi  9123  difinf  9267  fiint  9275  infssuni  9294  fsuppunbi  9335  r1pwALT  9791  djuexb  9854  alephprc  10044  fin1a2lem12  10356  axcclem  10402  zorn2lem4  10444  zornn0g  10450  grothomex  10774  grothprimlem  10778  addclprlem2  10962  axicn  11095  0mnnnnn0  12454  fcdmnn0fsupp  12479  pfxccatin12lem3  14632  pfxccat3  14634  swrdccat  14635  pfxccat3a  14638  swrdccat3blem  14639  swrdccat3b  14640  harmonic  15755  nprmi  16576  issubm  18628  idresefmnd  18723  mulgfval  18888  oppgsubm  19157  idrespermg  19207  issrg  19933  srgfcl  19941  opprsubrg  20291  resubdrg  21049  cpmidpmat  22259  kgencn  22944  kgencn2  22945  txdis1cn  23023  qtopres  23086  qtopcn  23102  cfinfil  23281  tgphaus  23505  xmeterval  23822  blval2  23955  metuel2  23958  iscvsp  24528  zclmncvs  24549  caucfil  24684  resscdrg  24759  finiunmbl  24945  iblre  25195  logno1  26028  rlimcnp2  26353  ppi2i  26555  gausslemma2dlem1a  26750  2lgslem4  26791  noxp1o  27048  usgredgffibi  28335  nbupgrel  28356  nbuhgr2vtx1edgb  28363  nbusgreledg  28364  nbusgrf1o0  28380  nb3grpr  28393  nb3grpr2  28394  nb3gr2nb  28395  cusgrsizeinds  28463  cusgrfi  28469  finsumvtxdg2size  28561  wlkp1lem1  28684  wlkp1lem7  28690  wlkp1lem8  28691  wwlks2onsym  28966  rusgrnumwwlks  28982  clwwlknclwwlkdifnum  28987  clwwlknonfin  29101  clwwlknonex2  29116  umgr3cyclex  29190  eupthp1  29223  eupth2eucrct  29224  frcond3  29276  frgr3v  29282  3vfriswmgr  29285  1to3vfriendship  29288  2pthfrgrrn  29289  3cyclfrgrrn1  29292  4cycl2v2nb  29296  frgrnbnb  29300  frgrncvvdeqlem3  29308  frgrncvvdeqlem6  29311  frgrhash2wsp  29339  fusgr2wsp2nb  29341  numclwwlk1  29368  avril1  29470  n0lplig  29488  hhph  30183  nonbooli  30656  pjss2i  30685  atssma  31383  isrrext  32670  hasheuni  32773  dmvlsiga  32817  measiuns  32905  eulerpartlemmf  33064  fineqvrep  33785  cusgr3cyclex  33817  resconn  33927  cvmlift2lem9  33992  rdgprc0  34454  bj-snsetex  35507  bj-tagex  35531  bj-0int  35645  poimirlem30  36181  ftc1anclem3  36226  ftc1anclem6  36229  rrnheibor  36369  rngo1cl  36471  isdrngo1  36488  dfcoeleqvrels  37156  islpln2ah  38085  lhpocnel2  38555  cdlemg31b0N  39230  cdlemg31b0a  39231  cdlemh  39353  cdlemk19w  39508  aks4d1lem1  40592  sticksstones4  40630  mzpclval  41106  wopprc  41412  dfac21  41451  uniel  41609  sucomisnotcard  41938  binomcxplemdvsum  42757  binomcxp  42759  mccl  43959  fprodcn  43961  stoweidlem17  44378  fourierdlem89  44556  fourierdlem90  44557  fourierdlem91  44558  fourierdlem100  44567  omeiunltfirp  44880  hoidmvlelem5  44960  issmf  45089  issmff  45095  smflimlem4  45135  smflim  45138  smflim2  45167  smflimsuplem1  45181  smflimsuplem8  45188  smflimsup  45189  aiotaexb  45441  aiotavb  45442  aovvdm  45537  aovvfunressn  45539  aovrcl  45541  aovvoveq  45544  aov0nbovbi  45547  fnotaovb  45550  prmdvdsfmtnof1lem1  45896  341fppr2  46046  9fppr8  46049  issubmgm  46203  zlmodzxzldeplem3  46703  itscnhlinecirc02p  46991