Theorem ax12el 36956

Description: Basis step for constructing a substitution instance of ax-c15 36903 without using ax-c15 36903. 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 1873	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ↔ (∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤))
2		elequ1 2113	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥))
3		elequ2 2121	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
4	2, 3	bitrd 278	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
5	4	adantl 482	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦))
6		ax-5 1913	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑣 → ∀𝑥 𝑣 ∈ 𝑣)
7		ax-5 1913	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → ∀𝑣 𝑦 ∈ 𝑦)
8		elequ1 2113	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣))
9		elequ2 2121	. . . . . . . . . . 11 ⊢ (𝑣 = 𝑦 → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
10	8, 9	bitrd 278	. . . . . . . . . 10 ⊢ (𝑣 = 𝑦 → (𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦))
11	6, 7, 10	dvelimf-o 36943	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥 𝑦 ∈ 𝑦))
12	4	biimprcd 249	. . . . . . . . . 10 ⊢ (𝑦 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
13	12	alimi 1814	. . . . . . . . 9 ⊢ (∀𝑥 𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥))
14	11, 13	syl6 35	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
15	14	adantr 481	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑦 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
16	5, 15	sylbid 239	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
17	16	adantl 482	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)))
18		elequ1 2113	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥))
19		elequ2 2121	. . . . . . . . 9 ⊢ (𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
20	18, 19	sylan9bb 510	. . . . . . . 8 ⊢ ((𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
21	20	sps-o 36922	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
22		nfa1-o 36929	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤)
23	21	imbi2d 341	. . . . . . . 8 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
24	22, 23	albid 2215	. . . . . . 7 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
25	21, 24	imbi12d 345	. . . . . 6 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
26	25	adantr 481	. . . . 5 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
27	17, 26	mpbid 231	. . . 4 ⊢ ((∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
28	27	exp32 421	. . 3 ⊢ (∀𝑥(𝑥 = 𝑧 ∧ 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
29	1, 28	sylbir 234	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
30		elequ1 2113	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
31	30	ad2antll 726	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤))
32		ax-c14 36905	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑤 → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤)))
33	32	impcom 408	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
34	33	adantrr 714	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥 𝑦 ∈ 𝑤))
35	30	biimprcd 249	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑤 → (𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
36	35	alimi 1814	. . . . . . 7 ⊢ (∀𝑥 𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤))
37	34, 36	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑦 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
38	31, 37	sylbid 239	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑤 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
39	38	adantll 711	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)))
40		elequ1 2113	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
41	40	sps-o 36922	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
42	41	imbi2d 341	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
43	42	dral2-o 36944	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
44	41, 43	imbi12d 345	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
45	44	ad2antrr 723	. . . 4 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑥 ∈ 𝑤)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
46	39, 45	mpbid 231	. . 3 ⊢ (((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
47	46	exp32 421	. 2 ⊢ ((∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
48		elequ2 2121	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
49	48	ad2antll 726	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))
50		ax-c14 36905	. . . . . . . . 9 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦)))
51	50	imp 407	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑦) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
52	51	adantrr 714	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥 𝑧 ∈ 𝑦))
53	48	biimprcd 249	. . . . . . . 8 ⊢ (𝑧 ∈ 𝑦 → (𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
54	53	alimi 1814	. . . . . . 7 ⊢ (∀𝑥 𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥))
55	52, 54	syl6 35	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
56	49, 55	sylbid 239	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
57	56	adantlr 712	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)))
58	19	sps-o 36922	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤))
59	58	imbi2d 341	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
60	59	dral2-o 36944	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑤 → (∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
61	58, 60	imbi12d 345	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑤 → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
62	61	ad2antlr 724	. . . 4 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → ((𝑧 ∈ 𝑥 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑥)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
63	57, 62	mpbid 231	. . 3 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) ∧ (¬ ∀𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
64	63	exp32 421	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
65		ax6ev 1973	. . . . 5 ⊢ ∃𝑢 𝑢 = 𝑤
66		ax6ev 1973	. . . . . . 7 ⊢ ∃𝑣 𝑣 = 𝑧
67		ax-1 6	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑢 → (𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
68	67	alrimiv 1930	. . . . . . . . . 10 ⊢ (𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢))
69		elequ1 2113	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
70		elequ2 2121	. . . . . . . . . . . . 13 ⊢ (𝑢 = 𝑤 → (𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
71	69, 70	sylan9bb 510	. . . . . . . . . . . 12 ⊢ ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
72	71	adantl 482	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
73		dveeq2-o 36947	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (𝑣 = 𝑧 → ∀𝑥 𝑣 = 𝑧))
74		dveeq2-o 36947	. . . . . . . . . . . . . . 15 ⊢ (¬ ∀𝑥 𝑥 = 𝑤 → (𝑢 = 𝑤 → ∀𝑥 𝑢 = 𝑤))
75	73, 74	im2anan9 620	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → ((𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤)))
76	75	imp 407	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
77		19.26 1873	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) ↔ (∀𝑥 𝑣 = 𝑧 ∧ ∀𝑥 𝑢 = 𝑤))
78	76, 77	sylibr 233	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤))
79		nfa1-o 36929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤)
80	71	sps-o 36922	. . . . . . . . . . . . . 14 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤))
81	80	imbi2d 341	. . . . . . . . . . . . 13 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → ((𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ (𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
82	79, 81	albid 2215	. . . . . . . . . . . 12 ⊢ (∀𝑥(𝑣 = 𝑧 ∧ 𝑢 = 𝑤) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
83	78, 82	syl 17	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢) ↔ ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
84	72, 83	imbi12d 345	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → ((𝑣 ∈ 𝑢 → ∀𝑥(𝑥 = 𝑦 → 𝑣 ∈ 𝑢)) ↔ (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
85	68, 84	mpbii 232	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) ∧ (𝑣 = 𝑧 ∧ 𝑢 = 𝑤)) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
86	85	exp32 421	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
87	86	exlimdv 1936	. . . . . . 7 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑣 𝑣 = 𝑧 → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
88	66, 87	mpi 20	. . . . . 6 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
89	88	exlimdv 1936	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (∃𝑢 𝑢 = 𝑤 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
90	65, 89	mpi 20	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))
91	90	a1d 25	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))
92	91	a1d 25	. 2 ⊢ ((¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑥 𝑥 = 𝑤) → (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤)))))
93	29, 47, 64, 92	4cases 1038	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝑥 = 𝑦 → (𝑧 ∈ 𝑤 → ∀𝑥(𝑥 = 𝑦 → 𝑧 ∈ 𝑤))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-c5 36897  ax-c4 36898  ax-c7 36899  ax-c10 36900  ax-c11 36901  ax-c9 36904  ax-c14 36905

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-nf 1787

This theorem is referenced by: (None)