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

Theorem elirr 4294
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  |-  -.  A  e.  A

Proof of Theorem elirr
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neldifsnd 3526 . . . . . . . . 9  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )  ->  -.  A  e.  ( _V  \  { A } ) )
2 simp1 915 . . . . . . . . . . 11  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  /\  x  =  A )  ->  A  e.  A )
3 eleq1 2116 . . . . . . . . . . . . . . . 16  |-  ( y  =  A  ->  (
y  e.  x  <->  A  e.  x ) )
4 eleq1 2116 . . . . . . . . . . . . . . . 16  |-  ( y  =  A  ->  (
y  e.  ( _V 
\  { A }
)  <->  A  e.  ( _V  \  { A }
) ) )
53, 4imbi12d 227 . . . . . . . . . . . . . . 15  |-  ( y  =  A  ->  (
( y  e.  x  ->  y  e.  ( _V 
\  { A }
) )  <->  ( A  e.  x  ->  A  e.  ( _V  \  { A } ) ) ) )
65spcgv 2657 . . . . . . . . . . . . . 14  |-  ( A  e.  x  ->  ( A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  -> 
( A  e.  x  ->  A  e.  ( _V 
\  { A }
) ) ) )
76pm2.43b 50 . . . . . . . . . . . . 13  |-  ( A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  -> 
( A  e.  x  ->  A  e.  ( _V 
\  { A }
) ) )
873ad2ant2 937 . . . . . . . . . . . 12  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  /\  x  =  A )  ->  ( A  e.  x  ->  A  e.  ( _V 
\  { A }
) ) )
9 eleq2 2117 . . . . . . . . . . . . . 14  |-  ( x  =  A  ->  ( A  e.  x  <->  A  e.  A ) )
109imbi1d 224 . . . . . . . . . . . . 13  |-  ( x  =  A  ->  (
( A  e.  x  ->  A  e.  ( _V 
\  { A }
) )  <->  ( A  e.  A  ->  A  e.  ( _V  \  { A } ) ) ) )
11103ad2ant3 938 . . . . . . . . . . . 12  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  /\  x  =  A )  ->  ( ( A  e.  x  ->  A  e.  ( _V  \  { A } ) )  <->  ( A  e.  A  ->  A  e.  ( _V  \  { A } ) ) ) )
128, 11mpbid 139 . . . . . . . . . . 11  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  /\  x  =  A )  ->  ( A  e.  A  ->  A  e.  ( _V 
\  { A }
) ) )
132, 12mpd 13 . . . . . . . . . 10  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  /\  x  =  A )  ->  A  e.  ( _V 
\  { A }
) )
14133expia 1117 . . . . . . . . 9  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )  ->  ( x  =  A  ->  A  e.  ( _V  \  { A } ) ) )
151, 14mtod 599 . . . . . . . 8  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )  ->  -.  x  =  A )
16 vex 2577 . . . . . . . . . 10  |-  x  e. 
_V
17 eldif 2955 . . . . . . . . . 10  |-  ( x  e.  ( _V  \  { A } )  <->  ( x  e.  _V  /\  -.  x  e.  { A } ) )
1816, 17mpbiran 858 . . . . . . . . 9  |-  ( x  e.  ( _V  \  { A } )  <->  -.  x  e.  { A } )
19 velsn 3420 . . . . . . . . 9  |-  ( x  e.  { A }  <->  x  =  A )
2018, 19xchbinx 617 . . . . . . . 8  |-  ( x  e.  ( _V  \  { A } )  <->  -.  x  =  A )
2115, 20sylibr 141 . . . . . . 7  |-  ( ( A  e.  A  /\  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )  ->  x  e.  ( _V  \  { A } ) )
2221ex 112 . . . . . 6  |-  ( A  e.  A  ->  ( A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  ->  x  e.  ( _V  \  { A } ) ) )
2322alrimiv 1770 . . . . 5  |-  ( A  e.  A  ->  A. x
( A. y ( y  e.  x  -> 
y  e.  ( _V 
\  { A }
) )  ->  x  e.  ( _V  \  { A } ) ) )
24 df-ral 2328 . . . . . . . 8  |-  ( A. y  e.  x  [
y  /  x ]
x  e.  ( _V 
\  { A }
)  <->  A. y ( y  e.  x  ->  [ y  /  x ] x  e.  ( _V  \  { A } ) ) )
25 clelsb3 2158 . . . . . . . . . 10  |-  ( [ y  /  x ]
x  e.  ( _V 
\  { A }
)  <->  y  e.  ( _V  \  { A } ) )
2625imbi2i 219 . . . . . . . . 9  |-  ( ( y  e.  x  ->  [ y  /  x ] x  e.  ( _V  \  { A }
) )  <->  ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )
2726albii 1375 . . . . . . . 8  |-  ( A. y ( y  e.  x  ->  [ y  /  x ] x  e.  ( _V  \  { A } ) )  <->  A. y
( y  e.  x  ->  y  e.  ( _V 
\  { A }
) ) )
2824, 27bitri 177 . . . . . . 7  |-  ( A. y  e.  x  [
y  /  x ]
x  e.  ( _V 
\  { A }
)  <->  A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) ) )
2928imbi1i 231 . . . . . 6  |-  ( ( A. y  e.  x  [ y  /  x ] x  e.  ( _V  \  { A }
)  ->  x  e.  ( _V  \  { A } ) )  <->  ( A. y ( y  e.  x  ->  y  e.  ( _V  \  { A } ) )  ->  x  e.  ( _V  \  { A } ) ) )
3029albii 1375 . . . . 5  |-  ( A. x ( A. y  e.  x  [ y  /  x ] x  e.  ( _V  \  { A } )  ->  x  e.  ( _V  \  { A } ) )  <->  A. x
( A. y ( y  e.  x  -> 
y  e.  ( _V 
\  { A }
) )  ->  x  e.  ( _V  \  { A } ) ) )
3123, 30sylibr 141 . . . 4  |-  ( A  e.  A  ->  A. x
( A. y  e.  x  [ y  /  x ] x  e.  ( _V  \  { A } )  ->  x  e.  ( _V  \  { A } ) ) )
32 ax-setind 4290 . . . 4  |-  ( A. x ( A. y  e.  x  [ y  /  x ] x  e.  ( _V  \  { A } )  ->  x  e.  ( _V  \  { A } ) )  ->  A. x  x  e.  ( _V  \  { A } ) )
3331, 32syl 14 . . 3  |-  ( A  e.  A  ->  A. x  x  e.  ( _V  \  { A } ) )
34 eleq1 2116 . . . 4  |-  ( x  =  A  ->  (
x  e.  ( _V 
\  { A }
)  <->  A  e.  ( _V  \  { A }
) ) )
3534spcgv 2657 . . 3  |-  ( A  e.  A  ->  ( A. x  x  e.  ( _V  \  { A } )  ->  A  e.  ( _V  \  { A } ) ) )
3633, 35mpd 13 . 2  |-  ( A  e.  A  ->  A  e.  ( _V  \  { A } ) )
37 neldifsnd 3526 . 2  |-  ( A  e.  A  ->  -.  A  e.  ( _V  \  { A } ) )
3836, 37pm2.65i 578 1  |-  -.  A  e.  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    <-> wb 102    /\ w3a 896   A.wal 1257    = wceq 1259    e. wcel 1409   [wsb 1661   A.wral 2323   _Vcvv 2574    \ cdif 2942   {csn 3403
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 554  ax-in2 555  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-setind 4290
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ne 2221  df-ral 2328  df-v 2576  df-dif 2948  df-sn 3409
This theorem is referenced by:  ordirr  4295  elirrv  4300  sucprcreg  4301  dtruex  4311  ordsoexmid  4314  onnmin  4320  ssnel  4321  onpsssuc  4323  ordtri2or2exmid  4324  reg3exmidlemwe  4331  nntri2  6104  nntri3  6106  nndceq  6108  nndcel  6109  phpelm  6359  fiunsnnn  6369  onunsnss  6386  snon0  6387
  Copyright terms: Public domain W3C validator