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 dtru in its proof. (Contributed by Mario Carneiro, 8-Oct-2016)

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

Proof

Step Hyp Ref Expression
1 dtru
 |-  -. 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 elsb4
 |-  ( [ z / x ] y e. x <-> y e. z )
9 elsb4
 |-  ( [ 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