Theorem eleq1i 2825

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-clel 2809

This theorem is referenced by:  eleq12i  2827  eqeltri  2830  eqneltri  2853  intexrab  5317  abssexg  5352  rmorabex  5435  otelxp  5698  xpsspw  5788  dfse2  6087  dfse3  6325  ordtri3or  6384  fressnfv  7149  fnotovb  7455  ovmpos  7553  abnex  7749  sucexb  7796  f1stres  8010  f2ndres  8011  elxp6  8020  ottpos  8233  dftpos4  8242  tfr2b  8408  tz7.48-3  8456  unfi  9183  difinf  9319  fiint  9336  fiintOLD  9337  infssuni  9356  fsuppunbi  9399  r1pwALT  9858  djuexb  9921  alephprc  10111  fin1a2lem12  10423  axcclem  10469  zorn2lem4  10511  zornn0g  10517  grothomex  10841  grothprimlem  10845  addclprlem2  11029  axicn  11162  0mnnnnn0  12531  fcdmnn0fsupp  12557  pfxccatin12lem3  14748  pfxccat3  14750  swrdccat  14751  pfxccat3a  14754  swrdccat3blem  14755  swrdccat3b  14756  harmonic  15873  nprmi  16706  issubmgm  18678  issubm  18779  idresefmnd  18875  mulgfval  19050  oppgsubm  19343  idrespermg  19390  issrg  20146  srgfcl  20154  subrngrng  20508  opprsubrng  20517  rhmimasubrng  20524  cntzsubrng  20525  opprsubrg  20551  rngridlmcl  21176  isridlrng  21178  isridl  21211  resubdrg  21566  cpmidpmat  22809  kgencn  23492  kgencn2  23493  txdis1cn  23571  qtopres  23634  qtopcn  23650  cfinfil  23829  tgphaus  24053  xmeterval  24369  blval2  24499  metuel2  24502  iscvsp  25077  zclmncvs  25098  caucfil  25233  resscdrg  25308  finiunmbl  25495  iblre  25745  dvfsumlem2  25983  logno1  26595  rlimcnp2  26926  ppi2i  27129  gausslemma2dlem1a  27326  2lgslem4  27367  noxp1o  27625  usgrexmpl  29188  usgredgffibi  29249  nbupgrel  29270  nbuhgr2vtx1edgb  29277  nbusgreledg  29278  nbusgrf1o0  29294  nb3grpr  29307  nb3grpr2  29308  nb3gr2nb  29309  cusgrsizeinds  29378  cusgrfi  29384  finsumvtxdg2size  29476  wlkp1lem1  29599  wlkp1lem7  29605  wlkp1lem8  29606  wwlks2onsym  29886  rusgrnumwwlks  29902  clwwlknclwwlkdifnum  29907  clwwlknonfin  30021  clwwlknonex2  30036  umgr3cyclex  30110  eupthp1  30143  eupth2eucrct  30144  frcond3  30196  frgr3v  30202  3vfriswmgr  30205  1to3vfriendship  30208  2pthfrgrrn  30209  3cyclfrgrrn1  30212  4cycl2v2nb  30216  frgrnbnb  30220  frgrncvvdeqlem3  30228  frgrncvvdeqlem6  30231  frgrhash2wsp  30259  fusgr2wsp2nb  30261  numclwwlk1  30288  avril1  30390  n0lplig  30410  hhph  31105  nonbooli  31578  pjss2i  31607  atssma  32305  isrrext  33977  hasheuni  34062  dmvlsiga  34106  measiuns  34194  eulerpartlemmf  34353  fineqvrep  35072  cusgr3cyclex  35104  resconn  35214  cvmlift2lem9  35279  rdgprc0  35757  bj-snsetex  36927  bj-tagex  36951  bj-0int  37065  poimirlem30  37620  ftc1anclem3  37665  ftc1anclem6  37668  rrnheibor  37807  rngo1cl  37909  isdrngo1  37926  dfcoeleqvrels  38585  islpln2ah  39514  lhpocnel2  39984  cdlemg31b0N  40659  cdlemg31b0a  40660  cdlemh  40782  cdlemk19w  40937  aks4d1lem1  42021  sticksstones4  42108  mzpclval  42695  wopprc  43001  dfac21  43037  uniel  43188  sucomisnotcard  43515  binomcxplemdvsum  44327  binomcxp  44329  mccl  45575  fprodcn  45577  stoweidlem17  45994  fourierdlem89  46172  fourierdlem90  46173  fourierdlem91  46174  fourierdlem100  46183  omeiunltfirp  46496  hoidmvlelem5  46576  issmf  46705  issmff  46711  smflimlem4  46751  smflim  46754  smflim2  46783  smflimsuplem1  46797  smflimsuplem8  46804  smflimsup  46805  aiotaexb  47066  aiotavb  47067  aovvdm  47162  aovvfunressn  47164  aovrcl  47166  aovvoveq  47169  aov0nbovbi  47172  fnotaovb  47175  prmdvdsfmtnof1lem1  47546  341fppr2  47696  9fppr8  47699  clnbupgrel  47796  grtriproplem  47899  grtrif1o  47902  grtriclwlk3  47905  usgrgrtrirex  47910  isubgr3stgrlem7  47932  usgrexmpl1  47974  usgrexmpl2  47979  gpgvtxedg0  48015  gpgvtxedg1  48016  gpgprismgr4cycllem11  48052  zlmodzxzldeplem3  48426  itscnhlinecirc02p  48713  fonex  48790