Theorem ax12el

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

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

Proof

Step	Hyp	Ref	Expression
1		19.26	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ↔ ( ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) )
2		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑥 ) )
3		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
4	2 3	bitrd	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
5	4	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑦 ∈ 𝑦 ) )
6		ax-5	⊢ ( 𝑣 ∈ 𝑣 → ∀ 𝑥 𝑣 ∈ 𝑣 )
7		ax-5	⊢ ( 𝑦 ∈ 𝑦 → ∀ 𝑣 𝑦 ∈ 𝑦 )
8		elequ1	⊢ ( 𝑣 = 𝑦 → ( 𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑣 ) )
9		elequ2	⊢ ( 𝑣 = 𝑦 → ( 𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦 ) )
10	8 9	bitrd	⊢ ( 𝑣 = 𝑦 → ( 𝑣 ∈ 𝑣 ↔ 𝑦 ∈ 𝑦 ) )
11	6 7 10	dvelimf-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 ∈ 𝑦 → ∀ 𝑥 𝑦 ∈ 𝑦 ) )
12	4	biimprcd	⊢ ( 𝑦 ∈ 𝑦 → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) )
13	12	alimi	⊢ ( ∀ 𝑥 𝑦 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) )
14	11 13	syl6	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑦 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) )
15	14	adantr	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑦 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) )
16	5 15	sylbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) → ( 𝑥 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) )
17	16	adantl	⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) )
18		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
19		elequ2	⊢ ( 𝑥 = 𝑤 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
20	18 19	sylan9bb	⊢ ( ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
21	20	sps-o	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( 𝑥 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
22		nfa1-o	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 )
23	21	imbi2d	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ↔ ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
24	22 23	albid	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
25	21 24	imbi12d	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ( 𝑥 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
26	25	adantr	⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑥 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
27	17 26	mpbid	⊢ ( ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
28	27	exp32	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 ∧ 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
29	1 28	sylbir	⊢ ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
30		elequ1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤 ) )
31	30	ad2antll	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝑤 ↔ 𝑦 ∈ 𝑤 ) )
32		ax-c14	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑦 ∈ 𝑤 → ∀ 𝑥 𝑦 ∈ 𝑤 ) ) )
33	32	impcom	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑦 ∈ 𝑤 → ∀ 𝑥 𝑦 ∈ 𝑤 ) )
34	33	adantrr	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑦 ∈ 𝑤 → ∀ 𝑥 𝑦 ∈ 𝑤 ) )
35	30	biimprcd	⊢ ( 𝑦 ∈ 𝑤 → ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) )
36	35	alimi	⊢ ( ∀ 𝑥 𝑦 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) )
37	34 36	syl6	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑦 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ) )
38	31 37	sylbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ) )
39	38	adantll	⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑥 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ) )
40		elequ1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
41	40	sps-o	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( 𝑥 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤 ) )
42	41	imbi2d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ↔ ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
43	42	dral2-o	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
44	41 43	imbi12d	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
45	44	ad2antrr	⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑥 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑥 ∈ 𝑤 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
46	39 45	mpbid	⊢ ( ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
47	46	exp32	⊢ ( ( ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
48		elequ2	⊢ ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
49	48	ad2antll	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦 ) )
50		ax-c14	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑦 → ∀ 𝑥 𝑧 ∈ 𝑦 ) ) )
51	50	imp	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑦 ) → ( 𝑧 ∈ 𝑦 → ∀ 𝑥 𝑧 ∈ 𝑦 ) )
52	51	adantrr	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑦 → ∀ 𝑥 𝑧 ∈ 𝑦 ) )
53	48	biimprcd	⊢ ( 𝑧 ∈ 𝑦 → ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) )
54	53	alimi	⊢ ( ∀ 𝑥 𝑧 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) )
55	52 54	syl6	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) )
56	49 55	sylbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) )
57	56	adantlr	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) )
58	19	sps-o	⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( 𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑤 ) )
59	58	imbi2d	⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
60	59	dral2-o	⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
61	58 60	imbi12d	⊢ ( ∀ 𝑥 𝑥 = 𝑤 → ( ( 𝑧 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
62	61	ad2antlr	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( ( 𝑧 ∈ 𝑥 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
63	57 62	mpbid	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ 𝑥 = 𝑦 ) ) → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
64	63	exp32	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
65		ax6ev	⊢ ∃ 𝑢 𝑢 = 𝑤
66		ax6ev	⊢ ∃ 𝑣 𝑣 = 𝑧
67		ax-1	⊢ ( 𝑣 ∈ 𝑢 → ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) )
68	67	alrimiv	⊢ ( 𝑣 ∈ 𝑢 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) )
69		elequ1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢 ) )
70		elequ2	⊢ ( 𝑢 = 𝑤 → ( 𝑧 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤 ) )
71	69 70	sylan9bb	⊢ ( ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤 ) )
72	71	adantl	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤 ) )
73		dveeq2-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( 𝑣 = 𝑧 → ∀ 𝑥 𝑣 = 𝑧 ) )
74		dveeq2-o	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( 𝑢 = 𝑤 → ∀ 𝑥 𝑢 = 𝑤 ) )
75	73 74	im2anan9	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) ) )
76	75	imp	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) )
77		19.26	⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ↔ ( ∀ 𝑥 𝑣 = 𝑧 ∧ ∀ 𝑥 𝑢 = 𝑤 ) )
78	76 77	sylibr	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) )
79		nfa1-o	⊢ Ⅎ 𝑥 ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 )
80	71	sps-o	⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑤 ) )
81	80	imbi2d	⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) ↔ ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
82	79 81	albid	⊢ ( ∀ 𝑥 ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
83	78 82	syl	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
84	72 83	imbi12d	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( ( 𝑣 ∈ 𝑢 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑣 ∈ 𝑢 ) ) ↔ ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
85	68 84	mpbii	⊢ ( ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ∧ ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑤 ) ) → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
86	85	exp32	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑣 = 𝑧 → ( 𝑢 = 𝑤 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
87	86	exlimdv	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ∃ 𝑣 𝑣 = 𝑧 → ( 𝑢 = 𝑤 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
88	66 87	mpi	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑢 = 𝑤 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
89	88	exlimdv	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ∃ 𝑢 𝑢 = 𝑤 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
90	65 89	mpi	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) )
91	90	a1d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )
92	91	a1d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) ) )
93	29 47 64 92	4cases	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( 𝑥 = 𝑦 → ( 𝑧 ∈ 𝑤 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝑧 ∈ 𝑤 ) ) ) )