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 206   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-clel 2808

This theorem is referenced by:  eleq12i  2826  eqeltri  2829  eqneltri  2852  intexrab  5327  abssexg  5362  rmorabex  5445  otelxp  5709  xpsspw  5799  dfse2  6098  dfse3  6336  ordtri3or  6395  fressnfv  7160  fnotovb  7465  ovmpos  7563  abnex  7759  sucexb  7806  f1stres  8020  f2ndres  8021  elxp6  8030  ottpos  8243  dftpos4  8252  tfr2b  8418  tz7.48-3  8466  unfi  9193  difinf  9331  fiint  9348  fiintOLD  9349  infssuni  9368  fsuppunbi  9411  r1pwALT  9868  djuexb  9931  alephprc  10121  fin1a2lem12  10433  axcclem  10479  zorn2lem4  10521  zornn0g  10527  grothomex  10851  grothprimlem  10855  addclprlem2  11039  axicn  11172  0mnnnnn0  12541  fcdmnn0fsupp  12567  pfxccatin12lem3  14753  pfxccat3  14755  swrdccat  14756  pfxccat3a  14759  swrdccat3blem  14760  swrdccat3b  14761  harmonic  15878  nprmi  16709  issubmgm  18685  issubm  18786  idresefmnd  18882  mulgfval  19057  oppgsubm  19350  idrespermg  19398  issrg  20154  srgfcl  20162  subrngrng  20519  opprsubrng  20528  rhmimasubrng  20535  cntzsubrng  20536  opprsubrg  20562  rngridlmcl  21190  isridlrng  21192  isridl  21225  resubdrg  21581  cpmidpmat  22828  kgencn  23511  kgencn2  23512  txdis1cn  23590  qtopres  23653  qtopcn  23669  cfinfil  23848  tgphaus  24072  xmeterval  24388  blval2  24520  metuel2  24523  iscvsp  25098  zclmncvs  25119  caucfil  25254  resscdrg  25329  finiunmbl  25516  iblre  25766  dvfsumlem2  26004  logno1  26615  rlimcnp2  26946  ppi2i  27149  gausslemma2dlem1a  27346  2lgslem4  27387  noxp1o  27645  usgrexmpl  29209  usgredgffibi  29270  nbupgrel  29291  nbuhgr2vtx1edgb  29298  nbusgreledg  29299  nbusgrf1o0  29315  nb3grpr  29328  nb3grpr2  29329  nb3gr2nb  29330  cusgrsizeinds  29399  cusgrfi  29405  finsumvtxdg2size  29497  wlkp1lem1  29620  wlkp1lem7  29626  wlkp1lem8  29627  wwlks2onsym  29907  rusgrnumwwlks  29923  clwwlknclwwlkdifnum  29928  clwwlknonfin  30042  clwwlknonex2  30057  umgr3cyclex  30131  eupthp1  30164  eupth2eucrct  30165  frcond3  30217  frgr3v  30223  3vfriswmgr  30226  1to3vfriendship  30229  2pthfrgrrn  30230  3cyclfrgrrn1  30233  4cycl2v2nb  30237  frgrnbnb  30241  frgrncvvdeqlem3  30249  frgrncvvdeqlem6  30252  frgrhash2wsp  30280  fusgr2wsp2nb  30282  numclwwlk1  30309  avril1  30411  n0lplig  30431  hhph  31126  nonbooli  31599  pjss2i  31628  atssma  32326  isrrext  33976  hasheuni  34061  dmvlsiga  34105  measiuns  34193  eulerpartlemmf  34352  fineqvrep  35084  cusgr3cyclex  35116  resconn  35226  cvmlift2lem9  35291  rdgprc0  35769  bj-snsetex  36939  bj-tagex  36963  bj-0int  37077  poimirlem30  37632  ftc1anclem3  37677  ftc1anclem6  37680  rrnheibor  37819  rngo1cl  37921  isdrngo1  37938  dfcoeleqvrels  38597  islpln2ah  39526  lhpocnel2  39996  cdlemg31b0N  40671  cdlemg31b0a  40672  cdlemh  40794  cdlemk19w  40949  aks4d1lem1  42038  sticksstones4  42125  mzpclval  42714  wopprc  43020  dfac21  43056  uniel  43207  sucomisnotcard  43534  binomcxplemdvsum  44346  binomcxp  44348  mccl  45585  fprodcn  45587  stoweidlem17  46004  fourierdlem89  46182  fourierdlem90  46183  fourierdlem91  46184  fourierdlem100  46193  omeiunltfirp  46506  hoidmvlelem5  46586  issmf  46715  issmff  46721  smflimlem4  46761  smflim  46764  smflim2  46793  smflimsuplem1  46807  smflimsuplem8  46814  smflimsup  46815  aiotaexb  47074  aiotavb  47075  aovvdm  47170  aovvfunressn  47172  aovrcl  47174  aovvoveq  47177  aov0nbovbi  47180  fnotaovb  47183  prmdvdsfmtnof1lem1  47544  341fppr2  47694  9fppr8  47697  clnbupgrel  47794  grtriproplem  47879  grtrif1o  47882  grtriclwlk3  47885  usgrgrtrirex  47890  isubgr3stgrlem7  47912  usgrexmpl1  47954  usgrexmpl2  47959  gpgvtxedg0  47994  gpgvtxedg1  47995  zlmodzxzldeplem3  48392  itscnhlinecirc02p  48679  fonex  48750