Theorem ax15 1357

Description: Axiom ax-15 1358 is redundant if we assume ax-17 969. 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. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 1355 and ax-17 969. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements.

This theorem should not be referenced in any proof. Instead, use ax-15 1358 below so that theorems needing ax-15 1358 can be more easily identified.

Assertion

Ref	Expression
ax15	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))

Proof of Theorem ax15

Step	Hyp	Ref	Expression
1		hbn1 1013	. . . . 5 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
2		dveel2 1355	. . . . 5 ⊢ (¬ ∀z z = y → (w ∈ y → ∀z w ∈ y))
3	1, 2	hbim1 1101	. . . 4 ⊢ ((¬ ∀z z = y → w ∈ y) → ∀z(¬ ∀z z = y → w ∈ y))
4		ax-17 969	. . . 4 ⊢ ((¬ ∀z z = y → x ∈ y) → ∀w(¬ ∀z z = y → x ∈ y))
5		elequ1 1134	. . . . 5 ⊢ (w = x → (w ∈ y ↔ x ∈ y))
6	5	imbi2d 611	. . . 4 ⊢ (w = x → ((¬ ∀z z = y → w ∈ y) ↔ (¬ ∀z z = y → x ∈ y)))
7	3, 4, 6	dvelimfALT 1151	. . 3 ⊢ (¬ ∀z z = x → ((¬ ∀z z = y → x ∈ y) → ∀z(¬ ∀z z = y → x ∈ y)))
8	1	19.21 1054	. . 3 ⊢ (∀z(¬ ∀z z = y → x ∈ y) ↔ (¬ ∀z z = y → ∀z x ∈ y))
9	7, 8	syl6ib 212	. 2 ⊢ (¬ ∀z z = x → ((¬ ∀z z = y → x ∈ y) → (¬ ∀z z = y → ∀z x ∈ y)))
10	9	pm2.86d 71	1 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))

Syntax hints:  ¬ wn 2   → wi 3  ∀wal 952   = wceq 954   ∈ wcel 956

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain