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 ¬ z z = x ¬ z z = y x y z x y

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz setvar z
1 0 cv setvar z
2 vx setvar x
3 2 cv setvar x
4 1 3 wceq wff z = x
5 4 0 wal wff z z = x
6 5 wn wff ¬ z z = x
7 vy setvar y
8 7 cv setvar y
9 1 8 wceq wff z = y
10 9 0 wal wff z z = y
11 10 wn wff ¬ z z = y
12 3 8 wcel wff x y
13 12 0 wal wff z x y
14 12 13 wi wff x y z x y
15 11 14 wi wff ¬ z z = y x y z x y
16 6 15 wi wff ¬ z z = x ¬ z z = y x y z x y