Theorem eleq1i 2820

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 2817	. 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 2702

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

This theorem is referenced by:  eleq12i  2822  eqeltri  2825  eqneltri  2848  intexrab  5305  abssexg  5340  rmorabex  5423  otelxp  5685  xpsspw  5775  dfse2  6074  dfse3  6312  ordtri3or  6367  fressnfv  7135  fnotovb  7442  ovmpos  7540  abnex  7736  sucexb  7783  f1stres  7995  f2ndres  7996  elxp6  8005  ottpos  8218  dftpos4  8227  tfr2b  8367  tz7.48-3  8415  unfi  9141  difinf  9267  fiint  9284  fiintOLD  9285  infssuni  9304  fsuppunbi  9347  r1pwALT  9806  djuexb  9869  alephprc  10059  fin1a2lem12  10371  axcclem  10417  zorn2lem4  10459  zornn0g  10465  grothomex  10789  grothprimlem  10793  addclprlem2  10977  axicn  11110  0mnnnnn0  12481  fcdmnn0fsupp  12507  pfxccatin12lem3  14704  pfxccat3  14706  swrdccat  14707  pfxccat3a  14710  swrdccat3blem  14711  swrdccat3b  14712  harmonic  15832  nprmi  16666  issubmgm  18636  issubm  18737  idresefmnd  18833  mulgfval  19008  oppgsubm  19301  idrespermg  19348  issrg  20104  srgfcl  20112  subrngrng  20466  opprsubrng  20475  rhmimasubrng  20482  cntzsubrng  20483  opprsubrg  20509  rngridlmcl  21134  isridlrng  21136  isridl  21169  resubdrg  21524  cpmidpmat  22767  kgencn  23450  kgencn2  23451  txdis1cn  23529  qtopres  23592  qtopcn  23608  cfinfil  23787  tgphaus  24011  xmeterval  24327  blval2  24457  metuel2  24460  iscvsp  25035  zclmncvs  25055  caucfil  25190  resscdrg  25265  finiunmbl  25452  iblre  25702  dvfsumlem2  25940  logno1  26552  rlimcnp2  26883  ppi2i  27086  gausslemma2dlem1a  27283  2lgslem4  27324  noxp1o  27582  usgrexmpl  29197  usgredgffibi  29258  nbupgrel  29279  nbuhgr2vtx1edgb  29286  nbusgreledg  29287  nbusgrf1o0  29303  nb3grpr  29316  nb3grpr2  29317  nb3gr2nb  29318  cusgrsizeinds  29387  cusgrfi  29393  finsumvtxdg2size  29485  wlkp1lem1  29608  wlkp1lem7  29614  wlkp1lem8  29615  wwlks2onsym  29895  rusgrnumwwlks  29911  clwwlknclwwlkdifnum  29916  clwwlknonfin  30030  clwwlknonex2  30045  umgr3cyclex  30119  eupthp1  30152  eupth2eucrct  30153  frcond3  30205  frgr3v  30211  3vfriswmgr  30214  1to3vfriendship  30217  2pthfrgrrn  30218  3cyclfrgrrn1  30221  4cycl2v2nb  30225  frgrnbnb  30229  frgrncvvdeqlem3  30237  frgrncvvdeqlem6  30240  frgrhash2wsp  30268  fusgr2wsp2nb  30270  numclwwlk1  30297  avril1  30399  n0lplig  30419  hhph  31114  nonbooli  31587  pjss2i  31616  atssma  32314  isrrext  33997  hasheuni  34082  dmvlsiga  34126  measiuns  34214  eulerpartlemmf  34373  fineqvrep  35092  onvf1odlem2  35098  onvf1odlem4  35100  cusgr3cyclex  35130  resconn  35240  cvmlift2lem9  35305  rdgprc0  35788  bj-snsetex  36958  bj-tagex  36982  bj-0int  37096  poimirlem30  37651  ftc1anclem3  37696  ftc1anclem6  37699  rrnheibor  37838  rngo1cl  37940  isdrngo1  37957  dfcoeleqvrels  38619  islpln2ah  39550  lhpocnel2  40020  cdlemg31b0N  40695  cdlemg31b0a  40696  cdlemh  40818  cdlemk19w  40973  aks4d1lem1  42057  sticksstones4  42144  mzpclval  42720  wopprc  43026  dfac21  43062  uniel  43213  sucomisnotcard  43540  binomcxplemdvsum  44351  binomcxp  44353  mccl  45603  fprodcn  45605  stoweidlem17  46022  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem100  46211  omeiunltfirp  46524  hoidmvlelem5  46604  issmf  46733  issmff  46739  smflimlem4  46779  smflim  46782  smflim2  46811  smflimsuplem1  46825  smflimsuplem8  46832  smflimsup  46833  aiotaexb  47094  aiotavb  47095  aovvdm  47190  aovvfunressn  47192  aovrcl  47194  aovvoveq  47197  aov0nbovbi  47200  fnotaovb  47203  mod2addne  47369  prmdvdsfmtnof1lem1  47589  341fppr2  47739  9fppr8  47742  clnbupgrel  47839  grtriproplem  47942  grtrif1o  47945  grtriclwlk3  47948  usgrgrtrirex  47953  isubgr3stgrlem7  47975  usgrexmpl1  48017  usgrexmpl2  48022  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedg2ov  48061  gpgedg2iv  48062  gpgprismgr4cycllem11  48099  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5  48117  pgnbgreunbgr  48119  pgn4cyclex  48120  zlmodzxzldeplem3  48495  itscnhlinecirc02p  48778  fonex  48859  idemb  49152