Theorem eleq1i 2827

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-clel 2811

This theorem is referenced by:  eleq12i  2829  eqeltri  2832  eqneltri  2855  intexrab  5292  abssexg  5327  rmorabex  5408  otelxp  5668  xpsspw  5758  dfse2  6059  dfse3  6294  ordtri3or  6349  fressnfv  7105  fnotovb  7410  ovmpos  7506  abnex  7702  sucexb  7749  f1stres  7957  f2ndres  7958  elxp6  7967  ottpos  8178  dftpos4  8187  tfr2b  8327  tz7.48-3  8375  unfi  9095  difinf  9211  fiint  9227  infssuni  9246  fsuppunbi  9292  r1pwALT  9758  djuexb  9821  alephprc  10009  fin1a2lem12  10321  axcclem  10367  zorn2lem4  10409  zornn0g  10415  grothomex  10740  grothprimlem  10744  addclprlem2  10928  axicn  11061  0mnnnnn0  12433  fcdmnn0fsupp  12459  pfxccatin12lem3  14655  pfxccat3  14657  swrdccat  14658  pfxccat3a  14661  swrdccat3blem  14662  swrdccat3b  14663  harmonic  15782  nprmi  16616  issubmgm  18627  issubm  18728  idresefmnd  18824  mulgfval  18999  oppgsubm  19291  idrespermg  19340  issrg  20123  srgfcl  20131  subrngrng  20483  opprsubrng  20492  rhmimasubrng  20499  cntzsubrng  20500  opprsubrg  20526  rngridlmcl  21172  isridlrng  21174  isridl  21207  resubdrg  21563  cpmidpmat  22817  kgencn  23500  kgencn2  23501  txdis1cn  23579  qtopres  23642  qtopcn  23658  cfinfil  23837  tgphaus  24061  xmeterval  24376  blval2  24506  metuel2  24509  iscvsp  25084  zclmncvs  25104  caucfil  25239  resscdrg  25314  finiunmbl  25501  iblre  25751  dvfsumlem2  25989  logno1  26601  rlimcnp2  26932  ppi2i  27135  gausslemma2dlem1a  27332  2lgslem4  27373  noxp1o  27631  usgrexmpl  29336  usgredgffibi  29397  nbupgrel  29418  nbuhgr2vtx1edgb  29425  nbusgreledg  29426  nbusgrf1o0  29442  nb3grpr  29455  nb3grpr2  29456  nb3gr2nb  29457  cusgrsizeinds  29526  cusgrfi  29532  finsumvtxdg2size  29624  wlkp1lem1  29745  wlkp1lem7  29751  wlkp1lem8  29752  wwlks2onsym  30033  rusgrnumwwlks  30050  clwwlknclwwlkdifnum  30055  clwwlknonfin  30169  clwwlknonex2  30184  umgr3cyclex  30258  eupthp1  30291  eupth2eucrct  30292  frcond3  30344  frgr3v  30350  3vfriswmgr  30353  1to3vfriendship  30356  2pthfrgrrn  30357  3cyclfrgrrn1  30360  4cycl2v2nb  30364  frgrnbnb  30368  frgrncvvdeqlem3  30376  frgrncvvdeqlem6  30379  frgrhash2wsp  30407  fusgr2wsp2nb  30409  numclwwlk1  30436  avril1  30538  n0lplig  30558  hhph  31253  nonbooli  31726  pjss2i  31755  atssma  32453  isrrext  34157  hasheuni  34242  dmvlsiga  34286  measiuns  34374  eulerpartlemmf  34532  fissorduni  35246  fineqvrep  35270  onvf1odlem2  35298  onvf1odlem4  35300  cusgr3cyclex  35330  resconn  35440  cvmlift2lem9  35505  rdgprc0  35985  bj-snsetex  37164  bj-tagex  37188  bj-0int  37306  poimirlem30  37851  ftc1anclem3  37896  ftc1anclem6  37899  rrnheibor  38038  rngo1cl  38140  isdrngo1  38157  dfcoeleqvrels  38878  islpln2ah  39809  lhpocnel2  40279  cdlemg31b0N  40954  cdlemg31b0a  40955  cdlemh  41077  cdlemk19w  41232  aks4d1lem1  42316  sticksstones4  42403  mzpclval  42967  wopprc  43272  dfac21  43308  uniel  43459  sucomisnotcard  43785  binomcxplemdvsum  44596  binomcxp  44598  mccl  45844  fprodcn  45846  stoweidlem17  46261  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem100  46450  omeiunltfirp  46763  hoidmvlelem5  46843  issmf  46972  issmff  46978  smflimlem4  47018  smflim  47021  smflim2  47050  smflimsuplem1  47064  smflimsuplem8  47071  smflimsup  47072  chnerlem1  47126  aiotaexb  47335  aiotavb  47336  aovvdm  47431  aovvfunressn  47433  aovrcl  47435  aovvoveq  47438  aov0nbovbi  47441  fnotaovb  47444  mod2addne  47610  prmdvdsfmtnof1lem1  47830  341fppr2  47980  9fppr8  47983  clnbupgrel  48080  grtriproplem  48185  grtrif1o  48188  grtriclwlk3  48191  usgrgrtrirex  48196  isubgr3stgrlem7  48218  grlimprclnbgr  48242  grlimprclnbgrvtx  48245  usgrexmpl1  48268  usgrexmpl2  48273  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedg2ov  48312  gpgedg2iv  48313  gpgprismgr4cycllem11  48351  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5  48369  pgnbgreunbgr  48371  pgn4cyclex  48372  zlmodzxzldeplem3  48748  itscnhlinecirc02p  49031  fonex  49112  idemb  49404