Description: A lemma for proving conditionless ZFC axioms. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 1-Jan-2002) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | nd2 | |- ( A. x x = y -> -. A. x z e. y ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elirrv | |- -. z e. z |
|
2 | stdpc4 | |- ( A. y z e. y -> [ z / y ] z e. y ) |
|
3 | 1 | nfnth | |- F/ y z e. z |
4 | elequ2 | |- ( y = z -> ( z e. y <-> z e. z ) ) |
|
5 | 3 4 | sbie | |- ( [ z / y ] z e. y <-> z e. z ) |
6 | 2 5 | sylib | |- ( A. y z e. y -> z e. z ) |
7 | 1 6 | mto | |- -. A. y z e. y |
8 | axc11 | |- ( A. x x = y -> ( A. x z e. y -> A. y z e. y ) ) |
|
9 | 7 8 | mtoi | |- ( A. x x = y -> -. A. x z e. y ) |