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 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑧 ∈ 𝑦 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elirrv | ⊢ ¬ 𝑧 ∈ 𝑧 | |
2 | stdpc4 | ⊢ ( ∀ 𝑦 𝑧 ∈ 𝑦 → [ 𝑧 / 𝑦 ] 𝑧 ∈ 𝑦 ) | |
3 | 1 | nfnth | ⊢ Ⅎ 𝑦 𝑧 ∈ 𝑧 |
4 | elequ2 | ⊢ ( 𝑦 = 𝑧 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑧 ) ) | |
5 | 3 4 | sbie | ⊢ ( [ 𝑧 / 𝑦 ] 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑧 ) |
6 | 2 5 | sylib | ⊢ ( ∀ 𝑦 𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑧 ) |
7 | 1 6 | mto | ⊢ ¬ ∀ 𝑦 𝑧 ∈ 𝑦 |
8 | axc11 | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 𝑧 ∈ 𝑦 → ∀ 𝑦 𝑧 ∈ 𝑦 ) ) | |
9 | 7 8 | mtoi | ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ¬ ∀ 𝑥 𝑧 ∈ 𝑦 ) |