Description: Axiom ax-c14 is redundant if we assume ax-5 . Remark 9.6 in Megill p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.
Note that w is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 and ax-5 . By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-Jun-1995) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc14 | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbn1 | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ∀ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑦 ) | |
| 2 | dveel2 | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑤 ∈ 𝑦 → ∀ 𝑧 𝑤 ∈ 𝑦 ) ) | |
| 3 | 1 2 | hbim1 | ⊢ ( ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑤 ∈ 𝑦 ) → ∀ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑤 ∈ 𝑦 ) ) |
| 4 | elequ1 | ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ 𝑦 ↔ 𝑥 ∈ 𝑦 ) ) | |
| 5 | 4 | imbi2d | ⊢ ( 𝑤 = 𝑥 → ( ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑤 ∈ 𝑦 ) ↔ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑥 ∈ 𝑦 ) ) ) |
| 6 | 3 5 | dvelim | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑥 ∈ 𝑦 ) → ∀ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑥 ∈ 𝑦 ) ) ) |
| 7 | nfa1 | ⊢ Ⅎ 𝑧 ∀ 𝑧 𝑧 = 𝑦 | |
| 8 | 7 | nfn | ⊢ Ⅎ 𝑧 ¬ ∀ 𝑧 𝑧 = 𝑦 |
| 9 | 8 | 19.21 | ⊢ ( ∀ 𝑧 ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑥 ∈ 𝑦 ) ↔ ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) |
| 10 | 6 9 | imbitrdi | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ( ¬ ∀ 𝑧 𝑧 = 𝑦 → 𝑥 ∈ 𝑦 ) → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) ) |
| 11 | 10 | pm2.86d | ⊢ ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥 ∈ 𝑦 → ∀ 𝑧 𝑥 ∈ 𝑦 ) ) ) |