Theorem eleq1i 2835

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-clel 2819

This theorem is referenced by:  eleq12i  2837  eqeltri  2840  eqneltri  2863  intexrab  5365  abssexg  5400  rmorabex  5480  otelxp  5744  xpsspw  5833  dfse2  6130  dfse3  6368  ordtri3or  6427  fressnfv  7194  fnotovb  7500  ovmpos  7598  abnex  7792  sucexb  7840  f1stres  8054  f2ndres  8055  elxp6  8064  ottpos  8277  dftpos4  8286  tfr2b  8452  tz7.48-3  8500  unfi  9238  difinf  9377  fiint  9394  fiintOLD  9395  infssuni  9414  fsuppunbi  9458  r1pwALT  9915  djuexb  9978  alephprc  10168  fin1a2lem12  10480  axcclem  10526  zorn2lem4  10568  zornn0g  10574  grothomex  10898  grothprimlem  10902  addclprlem2  11086  axicn  11219  0mnnnnn0  12585  fcdmnn0fsupp  12610  pfxccatin12lem3  14780  pfxccat3  14782  swrdccat  14783  pfxccat3a  14786  swrdccat3blem  14787  swrdccat3b  14788  harmonic  15907  nprmi  16736  issubmgm  18740  issubm  18838  idresefmnd  18934  mulgfval  19109  oppgsubm  19405  idrespermg  19453  issrg  20215  srgfcl  20223  subrngrng  20576  opprsubrng  20585  rhmimasubrng  20592  cntzsubrng  20593  opprsubrg  20621  rngridlmcl  21250  isridlrng  21252  isridl  21285  resubdrg  21649  cpmidpmat  22900  kgencn  23585  kgencn2  23586  txdis1cn  23664  qtopres  23727  qtopcn  23743  cfinfil  23922  tgphaus  24146  xmeterval  24463  blval2  24596  metuel2  24599  iscvsp  25180  zclmncvs  25201  caucfil  25336  resscdrg  25411  finiunmbl  25598  iblre  25849  dvfsumlem2  26087  logno1  26696  rlimcnp2  27027  ppi2i  27230  gausslemma2dlem1a  27427  2lgslem4  27468  noxp1o  27726  usgrexmpl  29298  usgredgffibi  29359  nbupgrel  29380  nbuhgr2vtx1edgb  29387  nbusgreledg  29388  nbusgrf1o0  29404  nb3grpr  29417  nb3grpr2  29418  nb3gr2nb  29419  cusgrsizeinds  29488  cusgrfi  29494  finsumvtxdg2size  29586  wlkp1lem1  29709  wlkp1lem7  29715  wlkp1lem8  29716  wwlks2onsym  29991  rusgrnumwwlks  30007  clwwlknclwwlkdifnum  30012  clwwlknonfin  30126  clwwlknonex2  30141  umgr3cyclex  30215  eupthp1  30248  eupth2eucrct  30249  frcond3  30301  frgr3v  30307  3vfriswmgr  30310  1to3vfriendship  30313  2pthfrgrrn  30314  3cyclfrgrrn1  30317  4cycl2v2nb  30321  frgrnbnb  30325  frgrncvvdeqlem3  30333  frgrncvvdeqlem6  30336  frgrhash2wsp  30364  fusgr2wsp2nb  30366  numclwwlk1  30393  avril1  30495  n0lplig  30515  hhph  31210  nonbooli  31683  pjss2i  31712  atssma  32410  isrrext  33946  hasheuni  34049  dmvlsiga  34093  measiuns  34181  eulerpartlemmf  34340  fineqvrep  35071  cusgr3cyclex  35104  resconn  35214  cvmlift2lem9  35279  rdgprc0  35757  bj-snsetex  36929  bj-tagex  36953  bj-0int  37067  poimirlem30  37610  ftc1anclem3  37655  ftc1anclem6  37658  rrnheibor  37797  rngo1cl  37899  isdrngo1  37916  dfcoeleqvrels  38577  islpln2ah  39506  lhpocnel2  39976  cdlemg31b0N  40651  cdlemg31b0a  40652  cdlemh  40774  cdlemk19w  40929  aks4d1lem1  42019  sticksstones4  42106  mzpclval  42681  wopprc  42987  dfac21  43023  uniel  43178  sucomisnotcard  43506  binomcxplemdvsum  44324  binomcxp  44326  mccl  45519  fprodcn  45521  stoweidlem17  45938  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem100  46127  omeiunltfirp  46440  hoidmvlelem5  46520  issmf  46649  issmff  46655  smflimlem4  46695  smflim  46698  smflim2  46727  smflimsuplem1  46741  smflimsuplem8  46748  smflimsup  46749  aiotaexb  47004  aiotavb  47005  aovvdm  47100  aovvfunressn  47102  aovrcl  47104  aovvoveq  47107  aov0nbovbi  47110  fnotaovb  47113  prmdvdsfmtnof1lem1  47458  341fppr2  47608  9fppr8  47611  clnbupgrel  47707  grtriproplem  47790  grtrif1o  47793  grtriclwlk3  47796  usgrgrtrirex  47799  usgrexmpl1  47837  usgrexmpl2  47842  zlmodzxzldeplem3  48231  itscnhlinecirc02p  48519