# Metamath Proof Explorer

## Theorem axc14

Description: Axiom ax-c14 is redundant if we assume ax-5 . Remark 9.6 in Megill p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.

Note that w is a dummy variable introduced in the proof. Its purpose is to satisfy the distinct variable requirements of dveel2 and ax-5 . By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 29-Jun-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc14 ${⊢}¬\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)$

### Proof

Step Hyp Ref Expression
1 hbn1 ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
2 dveel2 ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \left({w}\in {y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{w}\in {y}\right)$
3 1 2 hbim1 ${⊢}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {w}\in {y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {w}\in {y}\right)$
4 elequ1 ${⊢}{w}={x}\to \left({w}\in {y}↔{x}\in {y}\right)$
5 4 imbi2d ${⊢}{w}={x}\to \left(\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {w}\in {y}\right)↔\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {x}\in {y}\right)\right)$
6 3 5 dvelim ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {x}\in {y}\right)\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {x}\in {y}\right)\right)$
7 nfa1 ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
8 7 nfn ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}$
9 8 19.21 ${⊢}\forall {z}\phantom{\rule{.4em}{0ex}}\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {x}\in {y}\right)↔\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)$
10 6 9 syl6ib ${⊢}¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={x}\to \left(\left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to {x}\in {y}\right)\to \left(¬\forall {z}\phantom{\rule{.4em}{0ex}}{z}={y}\to \forall {z}\phantom{\rule{.4em}{0ex}}{x}\in {y}\right)\right)$
11 10 pm2.86d ${⊢}¬\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)$