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  37302  poimirlem30  37847  ftc1anclem3  37892  ftc1anclem6  37895  rrnheibor  38034  rngo1cl  38136  isdrngo1  38153  dfcoeleqvrels  38874  islpln2ah  39805  lhpocnel2  40275  cdlemg31b0N  40950  cdlemg31b0a  40951  cdlemh  41073  cdlemk19w  41228  aks4d1lem1  42312  sticksstones4  42399  mzpclval  42963  wopprc  43268  dfac21  43304  uniel  43455  sucomisnotcard  43781  binomcxplemdvsum  44592  binomcxp  44594  mccl  45840  fprodcn  45842  stoweidlem17  46257  fourierdlem89  46435  fourierdlem90  46436  fourierdlem91  46437  fourierdlem100  46446  omeiunltfirp  46759  hoidmvlelem5  46839  issmf  46968  issmff  46974  smflimlem4  47014  smflim  47017  smflim2  47046  smflimsuplem1  47060  smflimsuplem8  47067  smflimsup  47068  chnerlem1  47122  aiotaexb  47331  aiotavb  47332  aovvdm  47427  aovvfunressn  47429  aovrcl  47431  aovvoveq  47434  aov0nbovbi  47437  fnotaovb  47440  mod2addne  47606  prmdvdsfmtnof1lem1  47826  341fppr2  47976  9fppr8  47979  clnbupgrel  48076  grtriproplem  48181  grtrif1o  48184  grtriclwlk3  48187  usgrgrtrirex  48192  isubgr3stgrlem7  48214  grlimprclnbgr  48238  grlimprclnbgrvtx  48241  usgrexmpl1  48264  usgrexmpl2  48269  gpgvtxedg0  48305  gpgvtxedg1  48306  gpgedg2ov  48308  gpgedg2iv  48309  gpgprismgr4cycllem11  48347  pgnbgreunbgrlem1  48355  pgnbgreunbgrlem2lem3  48358  pgnbgreunbgrlem2  48359  pgnbgreunbgrlem4  48361  pgnbgreunbgrlem5  48365  pgnbgreunbgr  48367  pgn4cyclex  48368  zlmodzxzldeplem3  48744  itscnhlinecirc02p  49027  fonex  49108  idemb  49400