Theorem eleq1i 2832

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eleq12i  2834  eqeltri  2837  eqneltri  2860  intexrab  5347  abssexg  5382  rmorabex  5465  otelxp  5729  xpsspw  5819  dfse2  6118  dfse3  6357  ordtri3or  6416  fressnfv  7180  fnotovb  7483  ovmpos  7581  abnex  7777  sucexb  7824  f1stres  8038  f2ndres  8039  elxp6  8048  ottpos  8261  dftpos4  8270  tfr2b  8436  tz7.48-3  8484  unfi  9211  difinf  9349  fiint  9366  fiintOLD  9367  infssuni  9386  fsuppunbi  9429  r1pwALT  9886  djuexb  9949  alephprc  10139  fin1a2lem12  10451  axcclem  10497  zorn2lem4  10539  zornn0g  10545  grothomex  10869  grothprimlem  10873  addclprlem2  11057  axicn  11190  0mnnnnn0  12558  fcdmnn0fsupp  12584  pfxccatin12lem3  14770  pfxccat3  14772  swrdccat  14773  pfxccat3a  14776  swrdccat3blem  14777  swrdccat3b  14778  harmonic  15895  nprmi  16726  issubmgm  18715  issubm  18816  idresefmnd  18912  mulgfval  19087  oppgsubm  19381  idrespermg  19429  issrg  20185  srgfcl  20193  subrngrng  20550  opprsubrng  20559  rhmimasubrng  20566  cntzsubrng  20567  opprsubrg  20593  rngridlmcl  21227  isridlrng  21229  isridl  21262  resubdrg  21626  cpmidpmat  22879  kgencn  23564  kgencn2  23565  txdis1cn  23643  qtopres  23706  qtopcn  23722  cfinfil  23901  tgphaus  24125  xmeterval  24442  blval2  24575  metuel2  24578  iscvsp  25161  zclmncvs  25182  caucfil  25317  resscdrg  25392  finiunmbl  25579  iblre  25829  dvfsumlem2  26067  logno1  26678  rlimcnp2  27009  ppi2i  27212  gausslemma2dlem1a  27409  2lgslem4  27450  noxp1o  27708  usgrexmpl  29280  usgredgffibi  29341  nbupgrel  29362  nbuhgr2vtx1edgb  29369  nbusgreledg  29370  nbusgrf1o0  29386  nb3grpr  29399  nb3grpr2  29400  nb3gr2nb  29401  cusgrsizeinds  29470  cusgrfi  29476  finsumvtxdg2size  29568  wlkp1lem1  29691  wlkp1lem7  29697  wlkp1lem8  29698  wwlks2onsym  29978  rusgrnumwwlks  29994  clwwlknclwwlkdifnum  29999  clwwlknonfin  30113  clwwlknonex2  30128  umgr3cyclex  30202  eupthp1  30235  eupth2eucrct  30236  frcond3  30288  frgr3v  30294  3vfriswmgr  30297  1to3vfriendship  30300  2pthfrgrrn  30301  3cyclfrgrrn1  30304  4cycl2v2nb  30308  frgrnbnb  30312  frgrncvvdeqlem3  30320  frgrncvvdeqlem6  30323  frgrhash2wsp  30351  fusgr2wsp2nb  30353  numclwwlk1  30380  avril1  30482  n0lplig  30502  hhph  31197  nonbooli  31670  pjss2i  31699  atssma  32397  isrrext  34001  hasheuni  34086  dmvlsiga  34130  measiuns  34218  eulerpartlemmf  34377  fineqvrep  35109  cusgr3cyclex  35141  resconn  35251  cvmlift2lem9  35316  rdgprc0  35794  bj-snsetex  36964  bj-tagex  36988  bj-0int  37102  poimirlem30  37657  ftc1anclem3  37702  ftc1anclem6  37705  rrnheibor  37844  rngo1cl  37946  isdrngo1  37963  dfcoeleqvrels  38622  islpln2ah  39551  lhpocnel2  40021  cdlemg31b0N  40696  cdlemg31b0a  40697  cdlemh  40819  cdlemk19w  40974  aks4d1lem1  42063  sticksstones4  42150  mzpclval  42736  wopprc  43042  dfac21  43078  uniel  43229  sucomisnotcard  43557  binomcxplemdvsum  44374  binomcxp  44376  mccl  45613  fprodcn  45615  stoweidlem17  46032  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem100  46221  omeiunltfirp  46534  hoidmvlelem5  46614  issmf  46743  issmff  46749  smflimlem4  46789  smflim  46792  smflim2  46821  smflimsuplem1  46835  smflimsuplem8  46842  smflimsup  46843  aiotaexb  47101  aiotavb  47102  aovvdm  47197  aovvfunressn  47199  aovrcl  47201  aovvoveq  47204  aov0nbovbi  47207  fnotaovb  47210  prmdvdsfmtnof1lem1  47571  341fppr2  47721  9fppr8  47724  clnbupgrel  47821  grtriproplem  47906  grtrif1o  47909  grtriclwlk3  47912  usgrgrtrirex  47917  isubgr3stgrlem7  47939  usgrexmpl1  47981  usgrexmpl2  47986  gpgvtxedg0  48021  gpgvtxedg1  48022  zlmodzxzldeplem3  48419  itscnhlinecirc02p  48706