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

Theorem eleq2i 2151
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 2148 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 7 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wb 103   = wceq 1287  wcel 1436
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 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-4 1443  ax-17 1462  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078  df-clel 2081
This theorem is referenced by:  eleq12i  2152  eleqtri  2159  eleq2s  2179  hbxfreq  2191  abeq2i  2195  abeq1i  2196  nfceqi  2221  raleqbii  2386  rexeqbii  2387  rabeq2i  2612  elab2g  2753  elrabf  2760  elrab3t  2761  elrab2  2765  cbvsbc  2856  elin2  3177  dfnul2  3277  noel  3279  rabn0m  3299  rabeq0  3301  eltpg  3471  tpid3g  3538  oprcl  3629  elunirab  3649  elintrab  3683  exss  4028  elop  4032  opm  4035  brabsb  4062  brabga  4065  pofun  4113  elsuci  4204  elsucg  4205  elsuc2g  4206  ordsucim  4290  peano2  4383  elxp  4428  brab2a  4459  brab2ga  4481  elco  4570  elcnv  4581  dmmrnm  4623  elrnmptg  4655  opelres  4686  rninxp  4840  funco  5019  elfv  5266  nfvres  5300  fvopab3g  5340  fvmptssdm  5350  fmptco  5427  funfvima  5487  fliftel  5533  acexmidlema  5604  acexmidlemb  5605  acexmidlem2  5610  eloprabga  5692  elrnmpt2  5715  ovid  5718  offval  5820  xporderlem  5953  brtpos2  5970  issmo  6007  smores3  6012  tfrlem7  6036  tfrlem9  6038  tfr0dm  6041  tfri2  6085  rdgon  6105  freccllem  6121  frecfcllem  6123  frecsuclem  6125  el1o  6155  dif1o  6156  nnsucuniel  6210  elecg  6282  brecop  6334  erovlem  6336  oviec  6350  mapsncnv  6404  isfi  6430  enssdom  6431  map1  6481  xpcomco  6494  exmidpw  6576  fnfi  6596  djulclb  6691  djur  6701  eldju  6703  eldju2ndl  6707  eldju2ndr  6708  elni  6811  nlt1pig  6844  0nnq  6867  dfmq0qs  6932  dfplq0qs  6933  nqnq0  6944  elinp  6977  0npr  6986  ltdfpr  7009  nqprl  7054  nqpru  7055  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemfl  7078  mulnqprlemfu  7079  cauappcvgprlemladdru  7159  addsrpr  7235  mulsrpr  7236  opelcn  7308  opelreal  7309  elreal  7310  elreal2  7312  0ncn  7313  addcnsr  7315  mulcnsr  7316  addvalex  7325  peano1nnnn  7333  peano2nnnn  7334  xrlenlt  7495  1nn  8368  peano2nn  8369  elnn0  8608  elnnne0  8620  un0addcl  8639  un0mulcl  8640  elxnn0  8671  uztrn2  8968  elnnuz  8987  elnn0uz  8988  elq  9039  elxr  9179  elfzm1b  9442  fz01or  9455  frecfzennn  9761  inftonninf  9775  iseqfcl  9793  iseqfclt  9794  iser0  9847  iser0f  9848  hashinfom  10082  clim2iser  10617  clim2iser2  10618  iisermulc2  10620  iserile  10622  climserile  10625  divides  10673  dvdsflip  10727  infssuzex  10820  ialgrlemconst  10900  ialgrf  10902  bdceq  11171  bj-nntrans  11284  bj-nnelirr  11286  ss1oel2o  11326
  Copyright terms: Public domain W3C validator