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

Theorem eleq2i 2206
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 2203 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐶𝐵))
31, 2ax-mp 5 1 (𝐶𝐴𝐶𝐵)
Colors of variables: wff set class
Syntax hints:  wb 104   = wceq 1331  wcel 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  eleq12i  2207  eleqtri  2214  eleq2s  2234  hbxfreq  2246  abeq2i  2250  abeq1i  2251  nfceqi  2277  raleqbii  2447  rexeqbii  2448  rabeq2i  2683  elab2g  2831  elrabf  2838  elrab3t  2839  elrab2  2843  cbvsbcw  2936  cbvsbc  2937  elin2  3264  dfnul2  3365  noel  3367  rabn0m  3390  rabeq0  3392  eltpg  3569  tpid3g  3638  oprcl  3729  elunirab  3749  elintrab  3783  exss  4149  elop  4153  opm  4156  brabsb  4183  brabga  4186  pofun  4234  elsuci  4325  elsucg  4326  elsuc2g  4327  ordsucim  4416  peano2  4509  elxp  4556  brab2a  4592  brab2ga  4614  elco  4705  elcnv  4716  dmmrnm  4758  elrnmptg  4791  opelres  4824  rninxp  4982  funco  5163  elfv  5419  nfvres  5454  fvopab3g  5494  fvmptssdm  5505  fmptco  5586  funfvima  5649  fliftel  5694  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  eloprabga  5858  elrnmpo  5884  ovid  5887  offval  5989  xporderlem  6128  brtpos2  6148  issmo  6185  smores3  6190  tfrlem7  6214  tfrlem9  6216  tfr0dm  6219  tfri2  6263  rdgon  6283  freccllem  6299  frecfcllem  6301  frecsuclem  6303  el1o  6334  dif1o  6335  nnsucuniel  6391  elecg  6467  brecop  6519  erovlem  6521  oviec  6535  mapsncnv  6589  mptelixpg  6628  isfi  6655  enssdom  6656  map1  6706  xpcomco  6720  exmidpw  6802  fnfi  6825  fidcenumlemrks  6841  fidcenumlemrk  6842  djulclb  6940  eldju  6953  eldju2ndl  6957  eldju2ndr  6958  ctssdccl  6996  elni  7123  nlt1pig  7156  0nnq  7179  dfmq0qs  7244  dfplq0qs  7245  nqnq0  7256  elinp  7289  0npr  7298  ltdfpr  7321  nqprl  7366  nqpru  7367  addnqprlemfl  7374  addnqprlemfu  7375  mulnqprlemfl  7390  mulnqprlemfu  7391  cauappcvgprlemladdru  7471  suplocexprlemell  7528  addsrpr  7560  mulsrpr  7561  opelcn  7641  opelreal  7642  elreal  7643  elreal2  7645  0ncn  7646  addcnsr  7649  mulcnsr  7650  addvalex  7659  peano1nnnn  7667  peano2nnnn  7668  xrlenlt  7836  1nn  8738  peano2nn  8739  elnn0  8986  elnnne0  8998  un0addcl  9017  un0mulcl  9018  elxnn0  9049  uztrn2  9350  elnnuz  9369  elnn0uz  9370  elq  9421  elxr  9570  elfzm1b  9885  fz01or  9898  frecfzennn  10206  inftonninf  10221  seqf  10241  ser0  10294  ser0f  10295  hashinfom  10531  clim2ser  11113  clim2ser2  11114  isermulc2  11116  iserle  11118  climserle  11121  fsum3cvg3  11172  isumclim3  11199  isumadd  11207  sumsplitdc  11208  iserabs  11251  cvgcmpub  11252  isumshft  11266  isumsplit  11267  isumlessdc  11272  cvgratz  11308  cvgratgt0  11309  clim2prod  11315  clim2divap  11316  prodf1  11318  divides  11501  dvdsflip  11555  infssuzex  11648  ialgrlemconst  11730  ennnfonelemjn  11921  ennnfonelem1  11926  ennnfonelemdm  11939  istps  12208  lmss  12424  txuni2  12434  sinq34lt0t  12928  bdceq  13093  bj-nntrans  13202  bj-nnelirr  13204  ss1oel2o  13242  trilpolemisumle  13284
  Copyright terms: Public domain W3C validator