This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nfnid

Description: A setvar variable is not free from itself. This theorem is not true in a one-element domain, as illustrated by the use of dtruALT2 in its proof. (Contributed by Mario Carneiro, 8-Oct-2016)

Ref Expression
Assertion nfnid 
|- -. F/_ x x

Proof

Step Hyp Ref Expression
1 dtruALT2 
 |-  -. A. z z = w
2 ax-ext 
 |-  ( A. y ( y e. z <-> y e. w ) -> z = w )
3 2 sps 
 |-  ( A. w A. y ( y e. z <-> y e. w ) -> z = w )
4 3 alimi 
 |-  ( A. z A. w A. y ( y e. z <-> y e. w ) -> A. z z = w )
5 1 4 mto 
 |-  -. A. z A. w A. y ( y e. z <-> y e. w )
6 df-nfc 
 |-  ( F/_ x x <-> A. y F/ x y e. x )
7 sbnf2 
 |-  ( F/ x y e. x <-> A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) )
8 elsb2 
 |-  ( [ z / x ] y e. x <-> y e. z )
9 elsb2 
 |-  ( [ w / x ] y e. x <-> y e. w )
10 8 9 bibi12i 
 |-  ( ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> ( y e. z <-> y e. w ) )
11 10 2albii 
 |-  ( A. z A. w ( [ z / x ] y e. x <-> [ w / x ] y e. x ) <-> A. z A. w ( y e. z <-> y e. w ) )
12 7 11 bitri 
 |-  ( F/ x y e. x <-> A. z A. w ( y e. z <-> y e. w ) )
13 12 albii 
 |-  ( A. y F/ x y e. x <-> A. y A. z A. w ( y e. z <-> y e. w ) )
14 alrot3 
 |-  ( A. y A. z A. w ( y e. z <-> y e. w ) <-> A. z A. w A. y ( y e. z <-> y e. w ) )
15 6 13 14 3bitri 
 |-  ( F/_ x x <-> A. z A. w A. y ( y e. z <-> y e. w ) )
16 5 15 mtbir 
 |-  -. F/_ x x