Theorem eleq1i 2679

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

Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  eleq12i  2681  eqeltri  2684  intexrab  4750  abssexg  4777  rmorabex  4855  xpsspw  5156  dfse2  5418  ordtri3or  5672  fressnfv  6332  fnotovb  6592  ovmpt2s  6682  snnex  6862  pwexb  6867  sucexb  6901  iprc  6993  f1stres  7081  f2ndres  7082  elxp6  7091  ottpos  7249  dftpos4  7258  tfr2b  7379  tz7.48-3  7426  difinf  8115  fiint  8122  infssuni  8140  fsuppunbi  8179  r1pwALT  8592  alephprc  8805  fin1a2lem12  9116  axcclem  9162  zorn2lem4  9204  zornn0g  9210  grothomex  9530  grothprimlem  9534  addclprlem2  9718  axicn  9850  pnfnre  9960  mnfnre  9961  0mnnnnn0  11202  swrdccatin12lem3  13341  swrdccat3  13343  swrdccat  13344  swrdccat3blem  13346  swrdccat3b  13347  harmonic  14430  nprmi  15240  prmrec  15464  issubm  17170  oppgsubm  17615  idrespermg  17654  issrg  18330  srgfcl  18338  opprsubrg  18624  00lsp  18802  resubdrg  19773  cpmidpmat  20497  kgencn  21169  kgencn2  21170  txdis1cn  21248  qtopres  21311  qtopcn  21327  cfinfil  21507  tgphaus  21730  xmeterval  22047  blval2  22177  metuel2  22180  iscvsp  22736  zclmncvs  22756  caucfil  22889  resscdrg  22962  finiunmbl  23119  iblre  23366  logno1  24182  rlimcnp2  24493  ppi2i  24695  gausslemma2dlem1a  24890  2lgslem4  24931  nbgrasym  25968  nbgraf1olem3  25972  nbgraf1olem5  25974  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  cusgra2v  25991  cusgra3v  25993  uvtxnbgra  26021  uvtxnb  26025  cusconngra  26204  2wlkonotv  26404  rusgrasn  26472  frisusgranb  26524  frgra3v  26529  3vfriswmgra  26532  1to3vfriendship  26535  2pthfrgrarn  26536  3cyclfrgrarn1  26539  4cycl2v2nb  26543  frgranbnb  26547  frgrancvvdeqlem2  26558  frgrancvvdeqlem4  26560  frgrancvvdeqlem7  26563  frgrawopreglem4  26574  frgrawopreg  26576  frgrawopreg2  26578  usg2spot2nb  26592  numclwwlkovf2ex  26613  avril1  26711  hhph  27419  nonbooli  27894  pjss2i  27923  atssma  28621  isrrext  29372  hasheuni  29474  dmvlsiga  29519  measiuns  29607  eulerpartlemmf  29764  rescon  30482  cvmlift2lem9  30547  rdgprc0  30943  bj-snsetex  32144  bj-tagex  32168  bj-pinftynrr  32286  bj-minftynrr  32290  poimirlem30  32609  ftc1anclem3  32657  ftc1anclem6  32660  rrnheibor  32806  rngo1cl  32908  isdrngo1  32925  islpln2ah  33853  lhpocnel2  34323  cdlemg31b0N  35000  cdlemg31b0a  35001  cdlemh  35123  cdlemk19w  35278  mzpclval  36306  wopprc  36615  dfac21  36654  binomcxplemdvsum  37576  binomcxp  37578  mccl  38665  fprodcn  38667  stoweidlem17  38910  fourierdlem89  39088  fourierdlem90  39089  fourierdlem91  39090  fourierdlem100  39099  omeiunltfirp  39409  hoidmvlelem5  39489  issmf  39614  issmff  39620  smflimlem4  39660  smflim  39663  aovvdm  39914  aovvfunressn  39916  aovrcl  39918  aovvoveq  39921  aov0nbovbi  39924  fnotaovb  39927  prmdvdsfmtnof1lem1  40034  pfxccat3  40289  pfxccat3a  40292  nbupgrel  40567  nbuhgr2vtx1edgb  40574  nbusgreledg  40575  nbusgrf1o0  40597  nb3grpr  40610  nb3grpr2  40611  nb3gr2nb  40612  cusgrsizeinds  40668  cusgrfi  40674  1wlkp1lem1  40882  1wlkp1lem7  40888  1wlkp1lem8  40889  rusgrnumwwlks  41177  clwwlknclwwlkdifnum  41182  umgr3cyclex  41350  eupthp1  41384  eupth2eucrct  41385  frcond3  41440  frgr3v  41445  3vfriswmgr  41448  1to3vfriendship-av  41451  2pthfrgrrn  41452  3cyclfrgrrn1  41455  4cycl2v2nb-av  41459  frgrnbnb  41463  frgrncvvdeqlem2  41470  frgrncvvdeqlem4  41472  frgrncvvdeqlem7  41475  frgrwopreglem4  41484  frgrwopreg  41486  frgrwopreg2  41488  frgr2wwlkeqm  41496  frgrhash2wsp  41497  av-numclwwlkffin  41512  av-numclwwlkovf2ex  41517  issubmgm  41579  zlmodzxzldeplem3  42085