Theorem ax12el 33245

Description: Basis step for constructing a substitution instance of ax-c15 33192 without using ax-c15 33192. Atomic formula for membership predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax12el	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))

Proof of Theorem ax12el

Dummy variables 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26 1786	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		elequ1 1984	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
3		elequ2 1991	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
4	2, 3	bitrd 267	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
5	4	adantl 481	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
6		ax-5 1827	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑣 → ∀𝑥 𝑣 ∈ 𝑣)
7		ax-5 1827	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → ∀𝑣 𝑦 ∈ 𝑦)
8		elequ1 1984	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
9		elequ2 1991	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
10	8, 9	bitrd 267	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
11	6, 7, 10	dvelimf-o 33232	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥 𝑦 ∈ 𝑦))
12	4	biimprcd 239	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
13	12	alimi 1730	. . . . . . . . 9 ⊢ (∀𝑥 𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
14	11, 13	syl6 34	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
15	14	adantr 480	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
16	5, 15	sylbid 229	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
17	16	adantl 481	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
18		elequ1 1984	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
19		elequ2 1991	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
20	18, 19	sylan9bb 732	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
21	20	sps-o 33211	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
22		nfa1-o 33218	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
23	21	imbi2d 329	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
24	22, 23	albid 2077	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
25	21, 24	imbi12d 333	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
26	25	adantr 480	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
27	17, 26	mpbid 221	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
28	27	exp32 629	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
29	1, 28	sylbir 224	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
30		elequ1 1984	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
31	30	ad2antll 761	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
32		ax-c14 33194	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)))
33	32	impcom 445	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
34	33	adantrr 749	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
35	30	biimprcd 239	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑤 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
36	35	alimi 1730	. . . . . . 7 ⊢ (∀𝑥 𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
37	34, 36	syl6 34	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
38	31, 37	sylbid 229	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
39	38	adantll 746	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
40		elequ1 1984	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
41	40	sps-o 33211	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
42	41	imbi2d 329	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
43	42	dral2-o 33233	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
44	41, 43	imbi12d 333	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
45	44	ad2antrr 758	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
46	39, 45	mpbid 221	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
47	46	exp32 629	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
48		elequ2 1991	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
49	48	ad2antll 761	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
50		ax-c14 33194	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)))
51	50	imp 444	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
52	51	adantrr 749	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
53	48	biimprcd 239	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
54	53	alimi 1730	. . . . . . 7 ⊢ (∀𝑥 𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
55	52, 54	syl6 34	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
56	49, 55	sylbid 229	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
57	56	adantlr 747	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
58	19	sps-o 33211	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
59	58	imbi2d 329	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
60	59	dral2-o 33233	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
61	58, 60	imbi12d 333	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
62	61	ad2antlr 759	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
63	57, 62	mpbid 221	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
64	63	exp32 629	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
65		ax6ev 1877	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
66		ax6ev 1877	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
67		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑢 → (𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
68	67	alrimiv 1842	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
69		elequ1 1984	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
70		elequ2 1991	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
71	69, 70	sylan9bb 732	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
72	71	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
73		dveeq2-o 33236	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74		dveeq2-o 33236	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
75	73, 74	im2anan9 876	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
76	75	imp 444	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77		19.26 1786	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
78	76, 77	sylibr 223	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
79		nfa1-o 33218	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
80	71	sps-o 33211	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
81	80	imbi2d 329	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
82	79, 81	albid 2077	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
83	78, 82	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
84	72, 83	imbi12d 333	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
85	68, 84	mpbii 222	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
86	85	exp32 629	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
87	86	exlimdv 1848	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
88	66, 87	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
89	88	exlimdv 1848	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
90	65, 89	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
91	90	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
92	91	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
93	29, 47, 64, 92	4cases 987	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃wex 1695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-c5 33186  ax-c4 33187  ax-c7 33188  ax-c10 33189  ax-c11 33190  ax-c9 33193  ax-c14 33194

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by: (None)