# 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 ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)\right)$

### 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}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
6 5 wn ${wff}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}$
7 vy ${setvar}{y}$
8 7 cv ${setvar}{y}$
9 1 8 wceq ${wff}{z}={y}$
10 9 0 wal ${wff}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
11 10 wn ${wff}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
12 3 8 wcel ${wff}{x}\in {y}$
13 12 0 wal ${wff}\forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}$
14 12 13 wi ${wff}\left({x}\in {y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)$
15 11 14 wi ${wff}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)\right)$
16 6 15 wi ${wff}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({x}\in {y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)\right)\right)$