Theorem eleq1i 2829

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-clel 2817

This theorem is referenced by:  eleq12i  2831  eqneltri  2832  eqeltri  2835  intexrab  5259  abssexg  5300  rmorabex  5369  xpsspw  5708  dfse2  5997  ordtri3or  6283  fressnfv  7014  fnotovb  7305  ovmpos  7399  abnex  7585  sucexb  7631  f1stres  7828  f2ndres  7829  elxp6  7838  ottpos  8023  dftpos4  8032  tfr2b  8198  tz7.48-3  8245  unfi  8917  difinf  9014  fiint  9021  infssuni  9040  fsuppunbi  9079  r1pwALT  9535  djuexb  9598  alephprc  9786  fin1a2lem12  10098  axcclem  10144  zorn2lem4  10186  zornn0g  10192  grothomex  10516  grothprimlem  10520  addclprlem2  10704  axicn  10837  0mnnnnn0  12195  frnnn0fsupp  12220  pfxccatin12lem3  14373  pfxccat3  14375  swrdccat  14376  pfxccat3a  14379  swrdccat3blem  14380  swrdccat3b  14381  harmonic  15499  nprmi  16322  issubm  18357  idresefmnd  18453  mulgfval  18617  oppgsubm  18884  idrespermg  18934  issrg  19658  srgfcl  19666  opprsubrg  19960  resubdrg  20725  cpmidpmat  21930  kgencn  22615  kgencn2  22616  txdis1cn  22694  qtopres  22757  qtopcn  22773  cfinfil  22952  tgphaus  23176  xmeterval  23493  blval2  23624  metuel2  23627  iscvsp  24197  zclmncvs  24217  caucfil  24352  resscdrg  24427  finiunmbl  24613  iblre  24863  logno1  25696  rlimcnp2  26021  ppi2i  26223  gausslemma2dlem1a  26418  2lgslem4  26459  usgredgffibi  27594  nbupgrel  27615  nbuhgr2vtx1edgb  27622  nbusgreledg  27623  nbusgrf1o0  27639  nb3grpr  27652  nb3grpr2  27653  nb3gr2nb  27654  cusgrsizeinds  27722  cusgrfi  27728  finsumvtxdg2size  27820  wlkp1lem1  27943  wlkp1lem7  27949  wlkp1lem8  27950  wwlks2onsym  28224  rusgrnumwwlks  28240  clwwlknclwwlkdifnum  28245  clwwlknonfin  28359  clwwlknonex2  28374  umgr3cyclex  28448  eupthp1  28481  eupth2eucrct  28482  frcond3  28534  frgr3v  28540  3vfriswmgr  28543  1to3vfriendship  28546  2pthfrgrrn  28547  3cyclfrgrrn1  28550  4cycl2v2nb  28554  frgrnbnb  28558  frgrncvvdeqlem3  28566  frgrncvvdeqlem6  28569  frgrhash2wsp  28597  fusgr2wsp2nb  28599  numclwwlk1  28626  avril1  28728  n0lplig  28746  hhph  29441  nonbooli  29914  pjss2i  29943  atssma  30641  isrrext  31850  hasheuni  31953  dmvlsiga  31997  measiuns  32085  eulerpartlemmf  32242  fineqvrep  32964  cusgr3cyclex  32998  resconn  33108  cvmlift2lem9  33173  dfse3  33580  rdgprc0  33675  noxp1o  33793  bj-snsetex  35080  bj-tagex  35104  bj-0int  35199  poimirlem30  35734  ftc1anclem3  35779  ftc1anclem6  35782  rrnheibor  35922  rngo1cl  36024  isdrngo1  36041  dfcoeleqvrels  36661  islpln2ah  37490  lhpocnel2  37960  cdlemg31b0N  38635  cdlemg31b0a  38636  cdlemh  38758  cdlemk19w  38913  aks4d1lem1  39998  sticksstones4  40033  mzpclval  40463  wopprc  40768  dfac21  40807  binomcxplemdvsum  41862  binomcxp  41864  mccl  43029  fprodcn  43031  stoweidlem17  43448  fourierdlem89  43626  fourierdlem90  43627  fourierdlem91  43628  fourierdlem100  43637  omeiunltfirp  43947  hoidmvlelem5  44027  issmf  44151  issmff  44157  smflimlem4  44196  smflim  44199  smflim2  44226  smflimsuplem1  44240  smflimsuplem8  44247  smflimsup  44248  aiotaexb  44468  aiotavb  44469  aovvdm  44564  aovvfunressn  44566  aovrcl  44568  aovvoveq  44571  aov0nbovbi  44574  fnotaovb  44577  prmdvdsfmtnof1lem1  44924  341fppr2  45074  9fppr8  45077  issubmgm  45231  zlmodzxzldeplem3  45731  itscnhlinecirc02p  46019