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 ¬zz=x¬zz=yxyzxy

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz setvarz
1 0 cv setvarz
2 vx setvarx
3 2 cv setvarx
4 1 3 wceq wffz=x
5 4 0 wal wffzz=x
6 5 wn wff¬zz=x
7 vy setvary
8 7 cv setvary
9 1 8 wceq wffz=y
10 9 0 wal wffzz=y
11 10 wn wff¬zz=y
12 3 8 wcel wffxy
13 12 0 wal wffzxy
14 12 13 wi wffxyzxy
15 11 14 wi wff¬zz=yxyzxy
16 6 15 wi wff¬zz=x¬zz=yxyzxy