MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axacnd Structured version   Visualization version   GIF version

Theorem axacnd 9472
Description: A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)
Assertion
Ref Expression
axacnd 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))

Proof of Theorem axacnd
Dummy variable 𝑣 is distinct from all other variables.
StepHypRef Expression
1 axacndlem5 9471 . . . 4 𝑥𝑦𝑣(∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
2 nfnae 2351 . . . . . 6 𝑥 ¬ ∀𝑧 𝑧 = 𝑥
3 nfnae 2351 . . . . . 6 𝑥 ¬ ∀𝑧 𝑧 = 𝑦
4 nfnae 2351 . . . . . 6 𝑥 ¬ ∀𝑧 𝑧 = 𝑤
52, 3, 4nf3an 1871 . . . . 5 𝑥(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
6 nfnae 2351 . . . . . . 7 𝑦 ¬ ∀𝑧 𝑧 = 𝑥
7 nfnae 2351 . . . . . . 7 𝑦 ¬ ∀𝑧 𝑧 = 𝑦
8 nfnae 2351 . . . . . . 7 𝑦 ¬ ∀𝑧 𝑧 = 𝑤
96, 7, 8nf3an 1871 . . . . . 6 𝑦(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
10 nfnae 2351 . . . . . . . 8 𝑧 ¬ ∀𝑧 𝑧 = 𝑥
11 nfnae 2351 . . . . . . . 8 𝑧 ¬ ∀𝑧 𝑧 = 𝑦
12 nfnae 2351 . . . . . . . 8 𝑧 ¬ ∀𝑧 𝑧 = 𝑤
1310, 11, 12nf3an 1871 . . . . . . 7 𝑧(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
14 nfcvf 2817 . . . . . . . . . . . 12 (¬ ∀𝑧 𝑧 = 𝑦𝑧𝑦)
15143ad2ant2 1103 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑧𝑦)
16 nfcvd 2794 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑧𝑣)
1715, 16nfeld 2802 . . . . . . . . . 10 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦𝑣)
18 nfcvf 2817 . . . . . . . . . . . 12 (¬ ∀𝑧 𝑧 = 𝑤𝑧𝑤)
19183ad2ant3 1104 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑧𝑤)
2016, 19nfeld 2802 . . . . . . . . . 10 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑣𝑤)
2117, 20nfand 1866 . . . . . . . . 9 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦𝑣𝑣𝑤))
225, 21nfald 2201 . . . . . . . 8 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑥(𝑦𝑣𝑣𝑤))
23 nfnae 2351 . . . . . . . . . 10 𝑤 ¬ ∀𝑧 𝑧 = 𝑥
24 nfnae 2351 . . . . . . . . . 10 𝑤 ¬ ∀𝑧 𝑧 = 𝑦
25 nfnae 2351 . . . . . . . . . 10 𝑤 ¬ ∀𝑧 𝑧 = 𝑤
2623, 24, 25nf3an 1871 . . . . . . . . 9 𝑤(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
2715, 19nfeld 2802 . . . . . . . . . . . . . 14 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦𝑤)
28 nfcvf 2817 . . . . . . . . . . . . . . . 16 (¬ ∀𝑧 𝑧 = 𝑥𝑧𝑥)
29283ad2ant1 1102 . . . . . . . . . . . . . . 15 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑧𝑥)
3019, 29nfeld 2802 . . . . . . . . . . . . . 14 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑤𝑥)
3127, 30nfand 1866 . . . . . . . . . . . . 13 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦𝑤𝑤𝑥))
3221, 31nfand 1866 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)))
3326, 32nfexd 2203 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)))
3415, 19nfeqd 2801 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 = 𝑤)
3533, 34nfbid 1872 . . . . . . . . . 10 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
369, 35nfald 2201 . . . . . . . . 9 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
3726, 36nfexd 2203 . . . . . . . 8 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
3822, 37nfimd 1863 . . . . . . 7 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
39 nfcvd 2794 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑥𝑣)
40 nfcvf2 2818 . . . . . . . . . . . . 13 (¬ ∀𝑧 𝑧 = 𝑥𝑥𝑧)
41403ad2ant1 1102 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑥𝑧)
4239, 41nfeqd 2801 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑧)
435, 42nfan1 2106 . . . . . . . . . 10 𝑥((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
44 simpr 476 . . . . . . . . . . . 12 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → 𝑣 = 𝑧)
4544eleq2d 2716 . . . . . . . . . . 11 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑦𝑣𝑦𝑧))
4644eleq1d 2715 . . . . . . . . . . 11 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑣𝑤𝑧𝑤))
4745, 46anbi12d 747 . . . . . . . . . 10 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((𝑦𝑣𝑣𝑤) ↔ (𝑦𝑧𝑧𝑤)))
4843, 47albid 2128 . . . . . . . . 9 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑥(𝑦𝑣𝑣𝑤) ↔ ∀𝑥(𝑦𝑧𝑧𝑤)))
49 nfcvd 2794 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑤𝑣)
50 nfcvf2 2818 . . . . . . . . . . . . 13 (¬ ∀𝑧 𝑧 = 𝑤𝑤𝑧)
51503ad2ant3 1104 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑤𝑧)
5249, 51nfeqd 2801 . . . . . . . . . . 11 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑧)
5326, 52nfan1 2106 . . . . . . . . . 10 𝑤((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
54 nfcvd 2794 . . . . . . . . . . . . 13 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑦𝑣)
55 nfcvf2 2818 . . . . . . . . . . . . . 14 (¬ ∀𝑧 𝑧 = 𝑦𝑦𝑧)
56553ad2ant2 1103 . . . . . . . . . . . . 13 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → 𝑦𝑧)
5754, 56nfeqd 2801 . . . . . . . . . . . 12 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑧)
589, 57nfan1 2106 . . . . . . . . . . 11 𝑦((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
5947anbi1d 741 . . . . . . . . . . . . 13 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ ((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6053, 59exbid 2129 . . . . . . . . . . . 12 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ ∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥))))
6160bibi1d 332 . . . . . . . . . . 11 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6258, 61albid 2128 . . . . . . . . . 10 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6353, 62exbid 2129 . . . . . . . . 9 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
6448, 63imbi12d 333 . . . . . . . 8 (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
6564ex 449 . . . . . . 7 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (𝑣 = 𝑧 → ((∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
6613, 38, 65cbvald 2313 . . . . . 6 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑣(∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
679, 66albid 2128 . . . . 5 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑦𝑣(∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
685, 67exbid 2129 . . . 4 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∃𝑥𝑦𝑣(∀𝑥(𝑦𝑣𝑣𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑣𝑣𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))))
691, 68mpbii 223 . . 3 ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
70693exp 1283 . 2 (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (¬ ∀𝑧 𝑧 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))))
71 axacndlem2 9468 . . 3 (∀𝑥 𝑥 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7271aecoms 2345 . 2 (∀𝑧 𝑧 = 𝑥 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
73 axacndlem3 9469 . . 3 (∀𝑦 𝑦 = 𝑧 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
7473aecoms 2345 . 2 (∀𝑧 𝑧 = 𝑦 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
75 nfae 2349 . . . 4 𝑦𝑧 𝑧 = 𝑤
76 simpr 476 . . . . . . 7 ((𝑦𝑧𝑧𝑤) → 𝑧𝑤)
7776alimi 1779 . . . . . 6 (∀𝑥(𝑦𝑧𝑧𝑤) → ∀𝑥 𝑧𝑤)
78 nd3 9449 . . . . . . 7 (∀𝑧 𝑧 = 𝑤 → ¬ ∀𝑥 𝑧𝑤)
7978pm2.21d 118 . . . . . 6 (∀𝑧 𝑧 = 𝑤 → (∀𝑥 𝑧𝑤 → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8077, 79syl5 34 . . . . 5 (∀𝑧 𝑧 = 𝑤 → (∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8180axc4i 2169 . . . 4 (∀𝑧 𝑧 = 𝑤 → ∀𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8275, 81alrimi 2120 . . 3 (∀𝑧 𝑧 = 𝑤 → ∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
83 19.8a 2090 . . 3 (∀𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)) → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8482, 83syl 17 . 2 (∀𝑧 𝑧 = 𝑤 → ∃𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤)))
8570, 72, 74, 84pm2.61iii 179 1 𝑥𝑦𝑧(∀𝑥(𝑦𝑧𝑧𝑤) → ∃𝑤𝑦(∃𝑤((𝑦𝑧𝑧𝑤) ∧ (𝑦𝑤𝑤𝑥)) ↔ 𝑦 = 𝑤))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1054  wal 1521  wex 1744  wnfc 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-reg 8538  ax-ac 9319
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-eprel 5058  df-fr 5102
This theorem is referenced by:  zfcndac  9479  axacprim  31710
  Copyright terms: Public domain W3C validator