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
|- ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 vz
 |-  z
1 0 cv
 |-  z
2 vx
 |-  x
3 2 cv
 |-  x
4 1 3 wceq
 |-  z = x
5 4 0 wal
 |-  A. z z = x
6 5 wn
 |-  -. A. z z = x
7 vy
 |-  y
8 7 cv
 |-  y
9 1 8 wceq
 |-  z = y
10 9 0 wal
 |-  A. z z = y
11 10 wn
 |-  -. A. z z = y
12 3 8 wcel
 |-  x e. y
13 12 0 wal
 |-  A. z x e. y
14 12 13 wi
 |-  ( x e. y -> A. z x e. y )
15 11 14 wi
 |-  ( -. A. z z = y -> ( x e. y -> A. z x e. y ) )
16 6 15 wi
 |-  ( -. A. z z = x -> ( -. A. z z = y -> ( x e. y -> A. z x e. y ) ) )