Theorem eleq1i 2819

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eleq12i  2821  eqeltri  2824  eqneltri  2847  intexrab  5289  abssexg  5324  rmorabex  5407  otelxp  5667  xpsspw  5756  dfse2  6055  dfse3  6288  ordtri3or  6343  fressnfv  7098  fnotovb  7405  ovmpos  7501  abnex  7697  sucexb  7744  f1stres  7955  f2ndres  7956  elxp6  7965  ottpos  8176  dftpos4  8185  tfr2b  8325  tz7.48-3  8373  unfi  9095  difinf  9218  fiint  9235  fiintOLD  9236  infssuni  9255  fsuppunbi  9298  r1pwALT  9761  djuexb  9824  alephprc  10012  fin1a2lem12  10324  axcclem  10370  zorn2lem4  10412  zornn0g  10418  grothomex  10742  grothprimlem  10746  addclprlem2  10930  axicn  11063  0mnnnnn0  12434  fcdmnn0fsupp  12460  pfxccatin12lem3  14656  pfxccat3  14658  swrdccat  14659  pfxccat3a  14662  swrdccat3blem  14663  swrdccat3b  14664  harmonic  15784  nprmi  16618  issubmgm  18594  issubm  18695  idresefmnd  18791  mulgfval  18966  oppgsubm  19259  idrespermg  19308  issrg  20091  srgfcl  20099  subrngrng  20453  opprsubrng  20462  rhmimasubrng  20469  cntzsubrng  20470  opprsubrg  20496  rngridlmcl  21142  isridlrng  21144  isridl  21177  resubdrg  21533  cpmidpmat  22776  kgencn  23459  kgencn2  23460  txdis1cn  23538  qtopres  23601  qtopcn  23617  cfinfil  23796  tgphaus  24020  xmeterval  24336  blval2  24466  metuel2  24469  iscvsp  25044  zclmncvs  25064  caucfil  25199  resscdrg  25274  finiunmbl  25461  iblre  25711  dvfsumlem2  25949  logno1  26561  rlimcnp2  26892  ppi2i  27095  gausslemma2dlem1a  27292  2lgslem4  27333  noxp1o  27591  usgrexmpl  29226  usgredgffibi  29287  nbupgrel  29308  nbuhgr2vtx1edgb  29315  nbusgreledg  29316  nbusgrf1o0  29332  nb3grpr  29345  nb3grpr2  29346  nb3gr2nb  29347  cusgrsizeinds  29416  cusgrfi  29422  finsumvtxdg2size  29514  wlkp1lem1  29635  wlkp1lem7  29641  wlkp1lem8  29642  wwlks2onsym  29921  rusgrnumwwlks  29937  clwwlknclwwlkdifnum  29942  clwwlknonfin  30056  clwwlknonex2  30071  umgr3cyclex  30145  eupthp1  30178  eupth2eucrct  30179  frcond3  30231  frgr3v  30237  3vfriswmgr  30240  1to3vfriendship  30243  2pthfrgrrn  30244  3cyclfrgrrn1  30247  4cycl2v2nb  30251  frgrnbnb  30255  frgrncvvdeqlem3  30263  frgrncvvdeqlem6  30266  frgrhash2wsp  30294  fusgr2wsp2nb  30296  numclwwlk1  30323  avril1  30425  n0lplig  30445  hhph  31140  nonbooli  31613  pjss2i  31642  atssma  32340  isrrext  33969  hasheuni  34054  dmvlsiga  34098  measiuns  34186  eulerpartlemmf  34345  fineqvrep  35072  onvf1odlem2  35079  onvf1odlem4  35081  cusgr3cyclex  35111  resconn  35221  cvmlift2lem9  35286  rdgprc0  35769  bj-snsetex  36939  bj-tagex  36963  bj-0int  37077  poimirlem30  37632  ftc1anclem3  37677  ftc1anclem6  37680  rrnheibor  37819  rngo1cl  37921  isdrngo1  37938  dfcoeleqvrels  38600  islpln2ah  39531  lhpocnel2  40001  cdlemg31b0N  40676  cdlemg31b0a  40677  cdlemh  40799  cdlemk19w  40954  aks4d1lem1  42038  sticksstones4  42125  mzpclval  42701  wopprc  43006  dfac21  43042  uniel  43193  sucomisnotcard  43520  binomcxplemdvsum  44331  binomcxp  44333  mccl  45583  fprodcn  45585  stoweidlem17  46002  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem100  46191  omeiunltfirp  46504  hoidmvlelem5  46584  issmf  46713  issmff  46719  smflimlem4  46759  smflim  46762  smflim2  46791  smflimsuplem1  46805  smflimsuplem8  46812  smflimsup  46813  aiotaexb  47077  aiotavb  47078  aovvdm  47173  aovvfunressn  47175  aovrcl  47177  aovvoveq  47180  aov0nbovbi  47183  fnotaovb  47186  mod2addne  47352  prmdvdsfmtnof1lem1  47572  341fppr2  47722  9fppr8  47725  clnbupgrel  47822  grtriproplem  47927  grtrif1o  47930  grtriclwlk3  47933  usgrgrtrirex  47938  isubgr3stgrlem7  47960  grlimprclnbgr  47984  grlimprclnbgrvtx  47987  usgrexmpl1  48010  usgrexmpl2  48015  gpgvtxedg0  48051  gpgvtxedg1  48052  gpgedg2ov  48054  gpgedg2iv  48055  gpgprismgr4cycllem11  48093  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem2  48105  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5  48111  pgnbgreunbgr  48113  pgn4cyclex  48114  zlmodzxzldeplem3  48491  itscnhlinecirc02p  48774  fonex  48855  idemb  49148