Theorem ax12el 36238

Description: Basis step for constructing a substitution instance of ax-c15 36185 without using ax-c15 36185. 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 1871	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		elequ1 2118	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
3		elequ2 2126	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
4	2, 3	bitrd 282	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
5	4	adantl 485	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
6		ax-5 1911	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑣 → ∀𝑥 𝑣 ∈ 𝑣)
7		ax-5 1911	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → ∀𝑣 𝑦 ∈ 𝑦)
8		elequ1 2118	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
9		elequ2 2126	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
10	8, 9	bitrd 282	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
11	6, 7, 10	dvelimf-o 36225	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥 𝑦 ∈ 𝑦))
12	4	biimprcd 253	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
13	12	alimi 1813	. . . . . . . . 9 ⊢ (∀𝑥 𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
14	11, 13	syl6 35	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
15	14	adantr 484	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
16	5, 15	sylbid 243	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
17	16	adantl 485	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
18		elequ1 2118	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
19		elequ2 2126	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
20	18, 19	sylan9bb 513	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
21	20	sps-o 36204	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
22		nfa1-o 36211	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
23	21	imbi2d 344	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
24	22, 23	albid 2222	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
25	21, 24	imbi12d 348	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
26	25	adantr 484	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
27	17, 26	mpbid 235	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
28	27	exp32 424	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
29	1, 28	sylbir 238	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
30		elequ1 2118	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
31	30	ad2antll 728	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
32		ax-c14 36187	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)))
33	32	impcom 411	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
34	33	adantrr 716	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
35	30	biimprcd 253	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑤 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
36	35	alimi 1813	. . . . . . 7 ⊢ (∀𝑥 𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
37	34, 36	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
38	31, 37	sylbid 243	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
39	38	adantll 713	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
40		elequ1 2118	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
41	40	sps-o 36204	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
42	41	imbi2d 344	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
43	42	dral2-o 36226	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
44	41, 43	imbi12d 348	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
45	44	ad2antrr 725	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
46	39, 45	mpbid 235	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
47	46	exp32 424	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
48		elequ2 2126	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
49	48	ad2antll 728	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
50		ax-c14 36187	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)))
51	50	imp 410	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
52	51	adantrr 716	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
53	48	biimprcd 253	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
54	53	alimi 1813	. . . . . . 7 ⊢ (∀𝑥 𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
55	52, 54	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
56	49, 55	sylbid 243	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
57	56	adantlr 714	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
58	19	sps-o 36204	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
59	58	imbi2d 344	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
60	59	dral2-o 36226	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
61	58, 60	imbi12d 348	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
62	61	ad2antlr 726	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
63	57, 62	mpbid 235	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
64	63	exp32 424	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
65		ax6ev 1972	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
66		ax6ev 1972	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
67		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑢 → (𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
68	67	alrimiv 1928	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
69		elequ1 2118	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
70		elequ2 2126	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
71	69, 70	sylan9bb 513	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
72	71	adantl 485	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
73		dveeq2-o 36229	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74		dveeq2-o 36229	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
75	73, 74	im2anan9 622	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
76	75	imp 410	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77		19.26 1871	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
78	76, 77	sylibr 237	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
79		nfa1-o 36211	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
80	71	sps-o 36204	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
81	80	imbi2d 344	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
82	79, 81	albid 2222	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
83	78, 82	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
84	72, 83	imbi12d 348	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
85	68, 84	mpbii 236	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
86	85	exp32 424	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
87	86	exlimdv 1934	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
88	66, 87	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
89	88	exlimdv 1934	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
90	65, 89	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
91	90	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
92	91	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
93	29, 47, 64, 92	4cases 1036	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-13 2379  ax-c5 36179  ax-c4 36180  ax-c7 36181  ax-c10 36182  ax-c11 36183  ax-c9 36186  ax-c14 36187

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)