Theorem eleq1i 2829

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

Syntax hints:   ↔ wb 206   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  eleq12i  2831  eqeltri  2834  eqneltri  2857  intexrab  5352  abssexg  5387  rmorabex  5470  otelxp  5732  xpsspw  5821  dfse2  6120  dfse3  6358  ordtri3or  6417  fressnfv  7179  fnotovb  7482  ovmpos  7580  abnex  7775  sucexb  7823  f1stres  8036  f2ndres  8037  elxp6  8046  ottpos  8259  dftpos4  8268  tfr2b  8434  tz7.48-3  8482  unfi  9209  difinf  9346  fiint  9363  fiintOLD  9364  infssuni  9383  fsuppunbi  9426  r1pwALT  9883  djuexb  9946  alephprc  10136  fin1a2lem12  10448  axcclem  10494  zorn2lem4  10536  zornn0g  10542  grothomex  10866  grothprimlem  10870  addclprlem2  11054  axicn  11187  0mnnnnn0  12555  fcdmnn0fsupp  12581  pfxccatin12lem3  14766  pfxccat3  14768  swrdccat  14769  pfxccat3a  14772  swrdccat3blem  14773  swrdccat3b  14774  harmonic  15891  nprmi  16722  issubmgm  18727  issubm  18828  idresefmnd  18924  mulgfval  19099  oppgsubm  19395  idrespermg  19443  issrg  20205  srgfcl  20213  subrngrng  20566  opprsubrng  20575  rhmimasubrng  20582  cntzsubrng  20583  opprsubrg  20609  rngridlmcl  21244  isridlrng  21246  isridl  21279  resubdrg  21643  cpmidpmat  22894  kgencn  23579  kgencn2  23580  txdis1cn  23658  qtopres  23721  qtopcn  23737  cfinfil  23916  tgphaus  24140  xmeterval  24457  blval2  24590  metuel2  24593  iscvsp  25174  zclmncvs  25195  caucfil  25330  resscdrg  25405  finiunmbl  25592  iblre  25843  dvfsumlem2  26081  logno1  26692  rlimcnp2  27023  ppi2i  27226  gausslemma2dlem1a  27423  2lgslem4  27464  noxp1o  27722  usgrexmpl  29294  usgredgffibi  29355  nbupgrel  29376  nbuhgr2vtx1edgb  29383  nbusgreledg  29384  nbusgrf1o0  29400  nb3grpr  29413  nb3grpr2  29414  nb3gr2nb  29415  cusgrsizeinds  29484  cusgrfi  29490  finsumvtxdg2size  29582  wlkp1lem1  29705  wlkp1lem7  29711  wlkp1lem8  29712  wwlks2onsym  29987  rusgrnumwwlks  30003  clwwlknclwwlkdifnum  30008  clwwlknonfin  30122  clwwlknonex2  30137  umgr3cyclex  30211  eupthp1  30244  eupth2eucrct  30245  frcond3  30297  frgr3v  30303  3vfriswmgr  30306  1to3vfriendship  30309  2pthfrgrrn  30310  3cyclfrgrrn1  30313  4cycl2v2nb  30317  frgrnbnb  30321  frgrncvvdeqlem3  30329  frgrncvvdeqlem6  30332  frgrhash2wsp  30360  fusgr2wsp2nb  30362  numclwwlk1  30389  avril1  30491  n0lplig  30511  hhph  31206  nonbooli  31679  pjss2i  31708  atssma  32406  isrrext  33962  hasheuni  34065  dmvlsiga  34109  measiuns  34197  eulerpartlemmf  34356  fineqvrep  35087  cusgr3cyclex  35120  resconn  35230  cvmlift2lem9  35295  rdgprc0  35774  bj-snsetex  36945  bj-tagex  36969  bj-0int  37083  poimirlem30  37636  ftc1anclem3  37681  ftc1anclem6  37684  rrnheibor  37823  rngo1cl  37925  isdrngo1  37942  dfcoeleqvrels  38602  islpln2ah  39531  lhpocnel2  40001  cdlemg31b0N  40676  cdlemg31b0a  40677  cdlemh  40799  cdlemk19w  40954  aks4d1lem1  42043  sticksstones4  42130  mzpclval  42712  wopprc  43018  dfac21  43054  uniel  43205  sucomisnotcard  43533  binomcxplemdvsum  44350  binomcxp  44352  mccl  45553  fprodcn  45555  stoweidlem17  45972  fourierdlem89  46150  fourierdlem90  46151  fourierdlem91  46152  fourierdlem100  46161  omeiunltfirp  46474  hoidmvlelem5  46554  issmf  46683  issmff  46689  smflimlem4  46729  smflim  46732  smflim2  46761  smflimsuplem1  46775  smflimsuplem8  46782  smflimsup  46783  aiotaexb  47038  aiotavb  47039  aovvdm  47134  aovvfunressn  47136  aovrcl  47138  aovvoveq  47141  aov0nbovbi  47144  fnotaovb  47147  prmdvdsfmtnof1lem1  47508  341fppr2  47658  9fppr8  47661  clnbupgrel  47758  grtriproplem  47843  grtrif1o  47846  grtriclwlk3  47849  usgrgrtrirex  47852  isubgr3stgrlem7  47874  usgrexmpl1  47916  usgrexmpl2  47921  gpgvtxedg0  47955  gpgvtxedg1  47956  zlmodzxzldeplem3  48347  itscnhlinecirc02p  48634