Theorem eleq1i 2854

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-clel 2838

This theorem is referenced by:  eleq12i  2856  eqeltri  2859  eqneltri  2882  intexrab  5319  abssexg  5355  rmorabex  5443  otelxp  5707  xpsspw  5798  dfse2  6104  dfse3  6339  ordtri3or  6395  fressnfv  7159  fnotovb  7464  ovmpos  7560  abnex  7757  sucexb  7804  f1stres  8011  f2ndres  8012  elxp6  8021  ottpos  8233  dftpos4  8242  tfr2b  8384  tz7.48-3  8432  unfi  9156  difinf  9272  fiint  9287  infssuni  9304  fsuppunbi  9350  r1pwALT  9819  djuexb  9896  alephprc  10084  fin1a2lem12  10396  axcclem  10442  zorn2lem4  10484  zornn0g  10490  grothomex  10815  grothprimlem  10819  addclprlem2  11003  axicn  11136  0mnnnnn0  12537  fcdmnn0fsupp  12563  pfxccatin12lem3  14771  pfxccat3  14773  swrdccat  14774  pfxccat3a  14777  swrdccat3blem  14778  swrdccat3b  14779  harmonic  15915  nprmi  16748  issubmgm  18761  issubm  18862  idresefmnd  18959  mulgfval  19136  oppgsubm  19433  idrespermg  19482  issrg  20271  srgfcl  20279  subrngrng  20636  opprsubrng  20645  rhmimasubrng  20652  cntzsubrng  20653  opprsubrg  20679  rngridlmcl  21323  isridlrng  21325  isridl  21372  resubdrg  21739  cpmidpmat  23011  kgencn  23694  kgencn2  23695  txdis1cn  23773  qtopres  23836  qtopcn  23852  cfinfil  24031  tgphaus  24255  xmeterval  24570  blval2  24700  metuel2  24703  iscvsp  25268  zclmncvs  25288  caucfil  25423  resscdrg  25498  finiunmbl  25684  iblre  25934  dvfsumlem2  26167  logno1  26782  rlimcnp2  27112  ppi2i  27314  gausslemma2dlem1a  27510  2lgslem4  27551  noxp1o  27808  usgrexmpl  29594  usgredgffibi  29655  nbupgrel  29676  nbuhgr2vtx1edgb  29683  nbusgreledg  29684  nbusgrf1o0  29700  nb3grpr  29713  nb3grpr2  29714  nb3gr2nb  29715  cusgrsizeinds  29783  cusgrfi  29789  finsumvtxdg2size  29881  wlkp1lem1  30002  wlkp1lem7  30008  wlkp1lem8  30009  wwlks2onsym  30290  rusgrnumwwlks  30307  clwwlknclwwlkdifnum  30312  clwwlknonfin  30426  clwwlknonex2  30441  umgr3cyclex  30515  eupthp1  30548  eupth2eucrct  30549  frcond3  30601  frgr3v  30607  3vfriswmgr  30610  1to3vfriendship  30613  2pthfrgrrn  30614  3cyclfrgrrn1  30617  4cycl2v2nb  30621  frgrnbnb  30625  frgrncvvdeqlem3  30633  frgrncvvdeqlem6  30636  frgrhash2wsp  30664  fusgr2wsp2nb  30666  numclwwlk1  30693  avril1  30795  n0lplig  30816  hhph  31511  nonbooli  31984  pjss2i  32013  atssma  32711  isrrext  34371  hasheuni  34456  dmvlsiga  34500  measiuns  34588  eulerpartlemmf  34746  fissorduni  35461  fineqvrep  35508  onvf1odlem2  35569  onvf1odlem4  35571  cusgr3cyclex  35609  resconn  35719  cvmlift2lem9  35784  rdgprc0  36264  bj-snsetex  37580  bj-tagex  37604  bj-0int  37724  poimirlem30  38282  ftc1anclem3  38327  ftc1anclem6  38330  rrnheibor  38469  rngo1cl  38571  isdrngo1  38588  dfcoeleqvrels  39335  rnqmapeleldisjsim  39492  islpln2ah  40304  lhpocnel2  40774  cdlemg31b0N  41449  cdlemg31b0a  41450  cdlemh  41572  cdlemk19w  41727  aks4d1lem1  42810  sticksstones4  42897  mzpclval  43439  wopprc  43740  dfac21  43776  uniel  43927  sucomisnotcard  44253  binomcxplemdvsum  45048  binomcxp  45050  mccl  46297  fprodcn  46299  stoweidlem17  46714  fourierdlem89  46892  fourierdlem90  46893  fourierdlem91  46894  fourierdlem100  46903  omeiunltfirp  47216  hoidmvlelem5  47296  issmf  47425  issmff  47431  smflimlem4  47471  smflim  47474  smflim2  47503  smflimsuplem1  47517  smflimsuplem8  47524  smflimsup  47525  chnerlem1  47581  aiotaexb  47809  aiotavb  47810  aovvdm  47905  aovvfunressn  47907  aovrcl  47909  aovvoveq  47912  aov0nbovbi  47915  fnotaovb  47918  mod2addne  48090  prmdvdsfmtnof1lem1  48319  341fppr2  48482  9fppr8  48485  clnbupgrel  48582  grtriproplem  48687  grtrif1o  48690  grtriclwlk3  48693  usgrgrtrirex  48698  isubgr3stgrlem7  48720  grlimprclnbgr  48744  grlimprclnbgrvtx  48747  usgrexmpl1  48770  usgrexmpl2  48775  gpgvtxedg0  48811  gpgvtxedg1  48812  gpgedg2ov  48814  gpgedg2iv  48815  gpgprismgr4cycllem11  48853  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem2  48865  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5  48871  pgnbgreunbgr  48873  pgn4cyclex  48874  zlmodzxzldeplem3  49265  itscnhlinecirc02p  49548  fonex  49628  idemb  49920