Theorem ax12el 38943

Description: Basis step for constructing a substitution instance of ax-c15 38890 without using ax-c15 38890. 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 1870	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		elequ1 2115	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
3		elequ2 2123	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
4	2, 3	bitrd 279	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
5	4	adantl 481	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
6		ax-5 1910	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑣 → ∀𝑥 𝑣 ∈ 𝑣)
7		ax-5 1910	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → ∀𝑣 𝑦 ∈ 𝑦)
8		elequ1 2115	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
9		elequ2 2123	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
10	8, 9	bitrd 279	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
11	6, 7, 10	dvelimf-o 38930	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥 𝑦 ∈ 𝑦))
12	4	biimprcd 250	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
13	12	alimi 1811	. . . . . . . . 9 ⊢ (∀𝑥 𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
14	11, 13	syl6 35	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
15	14	adantr 480	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
16	5, 15	sylbid 240	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
17	16	adantl 481	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
18		elequ1 2115	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
19		elequ2 2123	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
20	18, 19	sylan9bb 509	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
21	20	sps-o 38909	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
22		nfa1-o 38916	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
23	21	imbi2d 340	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
24	22, 23	albid 2222	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
25	21, 24	imbi12d 344	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
26	25	adantr 480	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
27	17, 26	mpbid 232	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
28	27	exp32 420	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
29	1, 28	sylbir 235	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
30		elequ1 2115	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
31	30	ad2antll 729	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
32		ax-c14 38892	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)))
33	32	impcom 407	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
34	33	adantrr 717	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
35	30	biimprcd 250	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑤 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
36	35	alimi 1811	. . . . . . 7 ⊢ (∀𝑥 𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
37	34, 36	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
38	31, 37	sylbid 240	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
39	38	adantll 714	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
40		elequ1 2115	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
41	40	sps-o 38909	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
42	41	imbi2d 340	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
43	42	dral2-o 38931	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
44	41, 43	imbi12d 344	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
45	44	ad2antrr 726	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
46	39, 45	mpbid 232	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
47	46	exp32 420	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
48		elequ2 2123	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
49	48	ad2antll 729	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
50		ax-c14 38892	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)))
51	50	imp 406	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
52	51	adantrr 717	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
53	48	biimprcd 250	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
54	53	alimi 1811	. . . . . . 7 ⊢ (∀𝑥 𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
55	52, 54	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
56	49, 55	sylbid 240	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
57	56	adantlr 715	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
58	19	sps-o 38909	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
59	58	imbi2d 340	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
60	59	dral2-o 38931	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
61	58, 60	imbi12d 344	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
62	61	ad2antlr 727	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
63	57, 62	mpbid 232	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
64	63	exp32 420	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
65		ax6ev 1969	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
66		ax6ev 1969	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
67		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑢 → (𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
68	67	alrimiv 1927	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
69		elequ1 2115	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
70		elequ2 2123	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
71	69, 70	sylan9bb 509	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
72	71	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
73		dveeq2-o 38934	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74		dveeq2-o 38934	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
75	73, 74	im2anan9 620	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
76	75	imp 406	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77		19.26 1870	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
78	76, 77	sylibr 234	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
79		nfa1-o 38916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
80	71	sps-o 38909	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
81	80	imbi2d 340	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
82	79, 81	albid 2222	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
83	78, 82	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
84	72, 83	imbi12d 344	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
85	68, 84	mpbii 233	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
86	85	exp32 420	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
87	86	exlimdv 1933	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
88	66, 87	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
89	88	exlimdv 1933	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
90	65, 89	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
91	90	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
92	91	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
93	29, 47, 64, 92	4cases 1041	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-13 2377  ax-c5 38884  ax-c4 38885  ax-c7 38886  ax-c10 38887  ax-c11 38888  ax-c9 38891  ax-c14 38892

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by: (None)