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

Theorem elirr 4266
 Description: No class is a member of itself. Exercise 6 of [TakeutiZaring] p. 22. (Contributed by NM, 7-Aug-1994.) (Proof rewritten by Mario Carneiro and Jim Kingdon, 26-Nov-2018.)
Assertion
Ref Expression
elirr

Proof of Theorem elirr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neldifsnd 3498 . . . . . . . . 9
2 simp1 904 . . . . . . . . . . 11
3 eleq1 2100 . . . . . . . . . . . . . . . 16
4 eleq1 2100 . . . . . . . . . . . . . . . 16
53, 4imbi12d 223 . . . . . . . . . . . . . . 15
65spcgv 2640 . . . . . . . . . . . . . 14
76pm2.43b 46 . . . . . . . . . . . . 13
873ad2ant2 926 . . . . . . . . . . . 12
9 eleq2 2101 . . . . . . . . . . . . . 14
109imbi1d 220 . . . . . . . . . . . . 13
11103ad2ant3 927 . . . . . . . . . . . 12
128, 11mpbid 135 . . . . . . . . . . 11
132, 12mpd 13 . . . . . . . . . 10
14133expia 1106 . . . . . . . . 9
151, 14mtod 589 . . . . . . . 8
16 vex 2560 . . . . . . . . . 10
17 eldif 2927 . . . . . . . . . 10
1816, 17mpbiran 847 . . . . . . . . 9
19 velsn 3392 . . . . . . . . 9
2018, 19xchbinx 607 . . . . . . . 8
2115, 20sylibr 137 . . . . . . 7
2221ex 108 . . . . . 6
2322alrimiv 1754 . . . . 5
24 df-ral 2311 . . . . . . . 8
25 clelsb3 2142 . . . . . . . . . 10
2625imbi2i 215 . . . . . . . . 9
2726albii 1359 . . . . . . . 8
2824, 27bitri 173 . . . . . . 7
2928imbi1i 227 . . . . . 6
3029albii 1359 . . . . 5
3123, 30sylibr 137 . . . 4
32 ax-setind 4262 . . . 4
3331, 32syl 14 . . 3
34 eleq1 2100 . . . 4
3534spcgv 2640 . . 3
3633, 35mpd 13 . 2
37 neldifsnd 3498 . 2
3836, 37pm2.65i 568 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 97   wb 98   w3a 885  wal 1241   wceq 1243   wcel 1393  wsb 1645  wral 2306  cvv 2557   cdif 2914  csn 3375 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-setind 4262 This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-v 2559  df-dif 2920  df-sn 3381 This theorem is referenced by:  ordirr  4267  elirrv  4272  sucprcreg  4273  dtruex  4283  ordsoexmid  4286  onnmin  4292  ssnel  4293  onpsssuc  4295  ordtri2or2exmid  4296  reg3exmidlemwe  4303  nntri2  6073  nntri3  6075  nndceq  6077  nndcel  6078  phpelm  6328  fiunsnnn  6338  onunsnss  6355  snon0  6356
 Copyright terms: Public domain W3C validator