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

Theorem elirr 4456
 Description: No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. The reason that this theorem is marked as discouraged is a bit subtle. If we wanted to reduce usage of ax-setind 4452, we could redefine (df-iord 4288) to also require (df-frind 4254) and in that case any theorem related to irreflexivity of ordinals could use ordirr 4457 (which under that definition would presumably not need ax-setind 4452 to prove it). But since ordinals have not yet been defined that way, we cannot rely on the "don't add additional axiom use" feature of the minimizer to get theorems to use ordirr 4457. To encourage ordirr 4457 when possible, we mark this theorem as discouraged. (Contributed by NM, 7-Aug-1994.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 26-Nov-2018.) (New usage is discouraged.)
Assertion
Ref Expression
elirr

Proof of Theorem elirr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neldifsnd 3654 . . . . . . . . 9
2 simp1 981 . . . . . . . . . . 11
3 eleq1 2202 . . . . . . . . . . . . . . . 16
4 eleq1 2202 . . . . . . . . . . . . . . . 16
53, 4imbi12d 233 . . . . . . . . . . . . . . 15
65spcgv 2773 . . . . . . . . . . . . . 14
76pm2.43b 52 . . . . . . . . . . . . 13
873ad2ant2 1003 . . . . . . . . . . . 12
9 eleq2 2203 . . . . . . . . . . . . . 14
109imbi1d 230 . . . . . . . . . . . . 13
11103ad2ant3 1004 . . . . . . . . . . . 12
128, 11mpbid 146 . . . . . . . . . . 11
132, 12mpd 13 . . . . . . . . . 10
14133expia 1183 . . . . . . . . 9
151, 14mtod 652 . . . . . . . 8
16 vex 2689 . . . . . . . . . 10
17 eldif 3080 . . . . . . . . . 10
1816, 17mpbiran 924 . . . . . . . . 9
19 velsn 3544 . . . . . . . . 9
2018, 19xchbinx 671 . . . . . . . 8
2115, 20sylibr 133 . . . . . . 7
2221ex 114 . . . . . 6
2322alrimiv 1846 . . . . 5
24 df-ral 2421 . . . . . . . 8
25 clelsb3 2244 . . . . . . . . . 10
2625imbi2i 225 . . . . . . . . 9
2726albii 1446 . . . . . . . 8
2824, 27bitri 183 . . . . . . 7
2928imbi1i 237 . . . . . 6
3029albii 1446 . . . . 5
3123, 30sylibr 133 . . . 4
32 ax-setind 4452 . . . 4
3331, 32syl 14 . . 3
34 eleq1 2202 . . . 4
3534spcgv 2773 . . 3
3633, 35mpd 13 . 2
37 neldifsnd 3654 . 2
3836, 37pm2.65i 628 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wb 104   w3a 962  wal 1329   wceq 1331   wcel 1480  wsb 1735  wral 2416  cvv 2686   cdif 3068  csn 3527 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-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-setind 4452 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-v 2688  df-dif 3073  df-sn 3533 This theorem is referenced by:  ordirr  4457  elirrv  4463  sucprcreg  4464  ordsoexmid  4477  onnmin  4483  ssnel  4484  ordtri2or2exmid  4486  reg3exmidlemwe  4493  nntri2  6390  nntri3  6393  nndceq  6395  nndcel  6396  phpelm  6760  fiunsnnn  6775  onunsnss  6805  snon0  6824
 Copyright terms: Public domain W3C validator