ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eleq2i GIF version

Theorem eleq2i 2146
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
eleq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
eleq2i (𝐶𝐴𝐶𝐵)

Proof of Theorem eleq2i
StepHypRef Expression
1 eleq1i.1 . 2 𝐴 = 𝐵
2 eleq2 2143 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 7 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1285  wcel 1434
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075  df-clel 2078
This theorem is referenced by:  eleq12i  2147  eleqtri  2154  eleq2s  2174  hbxfreq  2186  abeq2i  2190  abeq1i  2191  nfceqi  2216  raleqbii  2379  rexeqbii  2380  rabeq2i  2599  elab2g  2741  elrabf  2748  elrab3t  2749  elrab2  2752  cbvsbc  2843  elin2  3157  dfnul2  3254  noel  3256  rabn0m  3273  rabeq0  3275  eltpg  3440  tpid3g  3507  oprcl  3596  elunirab  3616  elintrab  3650  exss  3984  elop  3988  opm  3991  brabsb  4018  brabga  4021  pofun  4069  elsuci  4160  elsucg  4161  elsuc2g  4162  ordsucim  4246  peano2  4338  elxp  4382  brab2a  4413  brab2ga  4435  elcnv  4534  dmmrnm  4576  elrnmptg  4608  opelres  4639  rninxp  4788  funco  4964  elfv  5201  nfvres  5232  fvopab3g  5271  fvmptssdm  5281  fmptco  5356  funfvima  5416  fliftel  5458  acexmidlema  5528  acexmidlemb  5529  acexmidlem2  5534  eloprabga  5616  elrnmpt2  5639  ovid  5642  offval  5744  xporderlem  5877  brtpos2  5894  issmo  5931  smores3  5936  tfrlem7  5960  tfrlem9  5962  tfr0dm  5965  tfri2  6009  rdgon  6029  freccllem  6045  frecfcllem  6047  frecsuclem  6049  el1o  6078  dif1o  6079  nnsucuniel  6132  elecg  6203  brecop  6255  erovlem  6257  oviec  6271  isfi  6300  enssdom  6301  xpcomco  6360  fnfi  6436  elni  6549  nlt1pig  6582  0nnq  6605  dfmq0qs  6670  dfplq0qs  6671  nqnq0  6682  elinp  6715  0npr  6724  ltdfpr  6747  nqprl  6792  nqpru  6793  addnqprlemfl  6800  addnqprlemfu  6801  mulnqprlemfl  6816  mulnqprlemfu  6817  cauappcvgprlemladdru  6897  addsrpr  6973  mulsrpr  6974  opelcn  7046  opelreal  7047  elreal  7048  elreal2  7050  0ncn  7051  addcnsr  7053  mulcnsr  7054  addvalex  7063  peano1nnnn  7071  peano2nnnn  7072  xrlenlt  7233  1nn  8106  peano2nn  8107  elnn0  8346  elnnne0  8358  un0addcl  8377  un0mulcl  8378  elxnn0  8409  uztrn2  8706  elnnuz  8725  elnn0uz  8726  elq  8777  elxr  8917  elfzm1b  9180  fz01or  9193  frecfzennn  9497  iseqfcl  9524  iseqfclt  9525  iser0  9557  iser0f  9558  sizeinf  9791  clim2iser  10302  clim2iser2  10303  iisermulc2  10305  iserile  10307  climserile  10310  divides  10331  dvdsflip  10385  infssuzex  10478  ialgrlemconst  10558  ialgrf  10560  bdceq  10776  bj-nntrans  10889  bj-nnelirr  10891
  Copyright terms: Public domain W3C validator