ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  id Structured version   Unicode version

Theorem id 19
Description: Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 20. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.)
Assertion
Ref Expression
id

Proof of Theorem id
StepHypRef Expression
1 ax-1 5 . 2
2 ax-1 5 . 2
31, 2mpd 13 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  idd  21  com12  27  pm2.27  35  pm2.43i  43  pm2.43d  44  pm2.43a  45  imim2  49  imim1i  54  imim1  70  pm2.04  76  pm2.86  94  pm3.2  126  biimprd  147  biimpcd  148  biimprcd  149  biid  160  bibi2i  216  imbi1  225  imbi2  226  bibi1  229  pm3.3  248  pm3.31  249  jctl  297  jctr  298  ancli  306  ancri  307  anc2li  312  anc2ri  313  anim12i  321  anim1i  323  anim2i  324  pm4.24  375  anass  381  mpdan  398  mpancom  399  pm5.32  426  anbi1  439  anbi2  440  mpan10  443  simpll  481  simplr  482  simprl  483  simprr  484  pm3.45  529  pm5.36  542  con2i  557  notnot1  559  con3i  561  biijust  569  con3  570  con2  571  notbii  593  pm5.19  621  olc  631  orc  632  pm2.621  665  pm1.2  672  orim1i  676  orim2i  677  pm2.41  692  pm2.42  693  pm2.4  694  pm4.44  695  orim2  702  orbi1  705  pm2.38  715  pm2.74  719  pm3.2ni  725  pm4.79dc  808  biantr  858  3anim1i  1089  3anim2i  1090  3anim3i  1091  mpd3an23  1233  trujust  1244  tru  1246  dftru2  1250  truimtru  1297  falimfal  1300  3impexp  1323  19.26  1367  19.8a  1479  19.9ht  1529  ax6blem  1537  19.36i  1559  19.41h  1572  equsb1  1665  sbieh  1670  dveeq2or  1694  spsbim  1721  2ax17  1755  dvelimALT  1883  dvelimfv  1884  dvelimor  1891  moanmo  1974  nfcvf  2196  necon3i  2247  nebidc  2279  vtoclgft  2598  eueq2dc  2708  cdeqcv  2752  ru  2757  sbcied2  2794  sbcralt  2828  sbcrext  2829  csbiebt  2880  csbied2  2887  cbvralcsf  2902  cbvrexcsf  2903  cbvreucsf  2904  cbvrabcsf  2905  ssid  2958  sspsstr  3044  psssstr  3045  difss2  3066  abvor0dc  3236  ssdifeq0  3299  ifbi  3342  rabsnt  3436  unisng  3588  dfnfc2  3589  a9evsep  3870  axnul  3873  intid  3951  opm  3962  opth1  3964  opth  3965  copsex4g  3975  0nelop  3976  moop2  3979  pocl  4031  swopo  4034  limeq  4080  suceq  4105  eusvnfb  4152  nn0eln0  4284  elvvuni  4347  coss1  4434  coss2  4435  dmxpm  4498  elrnmpt1  4528  soirri  4662  relcnvtr  4783  relssdmrn  4784  cnvpom  4803  fvsng  5302  isose  5403  riota2f  5432  acexmidlemab  5449  0neqopab  5492  ssoprab2  5503  caovcld  5596  caovcomd  5599  caovassd  5602  caovcand  5605  caovordid  5609  caovordd  5611  caovdid  5618  caovdird  5621  caovimo  5636  grprinvlem  5637  grprinvd  5638  f1opw  5649  caofref  5674  caofinvl  5675  xpexgALT  5702  op1stg  5719  op2ndg  5720  releldm2  5753  elopabi  5763  dfmpt2  5786  smoeq  5846  rdgisucinc  5912  rdg0g  5915  oacl  5979  nna0r  5996  nnmsucr  6006  ercnv  6063  swoord1  6071  swoord2  6072  eqer  6074  ider  6075  iinerm  6114  brecop  6132  en1bg  6216  fundmeng  6223  xpsneng  6232  mulidnq  6373  ltsonq  6382  halfnqq  6393  nqnq0pi  6420  nq02m  6447  cauappcvgprlemm  6616  cauappcvgprlemloc  6623  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  cauappcvgprlem2  6631  cauappcvgpr  6633  ltposr  6671  0idsr  6675  1idsr  6676  ax1rid  6741  ax0id  6742  axpre-ltirr  6746  mulid1  6802  1p1times  6924  cnegexlem3  6965  pncan1  7151  npcan1  7152  kcnktkm1cn  7156  apirr  7369  recexap  7396  eqneg  7470  lediv2a  7622  nn1m1nn  7693  add1p1  7931  sub1m1  7932  cnm2m1cnm3  7933  nn0addcl  7973  nn0mulcl  7974  zadd2cl  8123  nltpnft  8480  ngtmnft  8481  xrrebnd  8482  xnegneg  8496  fzss1  8676  fzssp1  8680  fzshftral  8720  0elfz  8727  nn0fz0  8728  elfz0add  8729  fz0tp  8731  elfzoelz  8754  fzoval  8755  fzoss2  8778  fzossrbm1  8779  fzouzsplit  8785  elfzo1  8796  fzonn0p1  8817  fzossfzop1  8818  fzoend  8828  fzosplitsn  8839  frec2uzltd  8850  frec2uzrand  8852  uzenom  8863  frecfzennn  8864  iseqeq1  8874  m1expcl2  8911  reval  9057  imval  9058  crim  9066  replim  9067  absval  9190  sqrt0  9193  bj-ex  9217  bdth  9266  bj-dcbi  9359
  Copyright terms: Public domain W3C validator