Metamath Proof Explorer


Axiom ax-c14

Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in Megill p. 448 (p. 16 of the preprint). It is redundant if we include ax-5 ; see Theorem axc14 . Alternately, ax-5 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-5 . We retain ax-c14 here to provide completeness for systems with the simpler metalogic that results from omitting ax-5 , which might be easier to study for some theoretical purposes.

This axiom is obsolete and should no longer be used. It is proved above as Theorem axc14 . (Contributed by NM, 24-Jun-1993) (New usage is discouraged.)

Ref Expression
Assertion ax-c14 ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz 𝑧
1 0 cv 𝑧
2 vx 𝑥
3 2 cv 𝑥
4 1 3 wceq 𝑧 = 𝑥
5 4 0 wal 𝑧 𝑧 = 𝑥
6 5 wn ¬ ∀ 𝑧 𝑧 = 𝑥
7 vy 𝑦
8 7 cv 𝑦
9 1 8 wceq 𝑧 = 𝑦
10 9 0 wal 𝑧 𝑧 = 𝑦
11 10 wn ¬ ∀ 𝑧 𝑧 = 𝑦
12 3 8 wcel 𝑥𝑦
13 12 0 wal 𝑧 𝑥𝑦
14 12 13 wi ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 )
15 11 14 wi ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) )
16 6 15 wi ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → ( 𝑥𝑦 → ∀ 𝑧 𝑥𝑦 ) ) )