Metamath Proof Explorer


Theorem aceq1

Description: Equivalence of two versions of the Axiom of Choice ax-ac . The proof uses neither AC nor the Axiom of Regularity. The right-hand side expresses our AC with the fewest number of different variables. (Contributed by NM, 5-Apr-2004)

Ref Expression
Assertion aceq1 ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑤 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 biidd ( 𝑤 = 𝑡 → ( ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ) )
2 1 cbvralvw ( ∀ 𝑤 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∀ 𝑡 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) )
3 elequ1 ( 𝑣 = 𝑧 → ( 𝑣𝑢𝑧𝑢 ) )
4 3 anbi2d ( 𝑣 = 𝑧 → ( ( 𝑢𝑣𝑢 ) ↔ ( 𝑢𝑧𝑢 ) ) )
5 4 rexbidv ( 𝑣 = 𝑧 → ( ∃ 𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∃ 𝑢𝑦 ( 𝑢𝑧𝑢 ) ) )
6 5 cbvreuvw ( ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) )
7 6 ralbii ( ∀ 𝑡 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∀ 𝑡 ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) )
8 2 7 bitri ( ∀ 𝑤 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∀ 𝑡 ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) )
9 8 ralbii ( ∀ 𝑥𝑤 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ↔ ∀ 𝑥𝑡 ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) )
10 elequ1 ( 𝑧 = → ( 𝑧𝑢𝑢 ) )
11 10 anbi1d ( 𝑧 = → ( ( 𝑧𝑢𝑣𝑢 ) ↔ ( 𝑢𝑣𝑢 ) ) )
12 11 rexbidv ( 𝑧 = → ( ∃ 𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑢𝑦 ( 𝑢𝑣𝑢 ) ) )
13 12 reueqd ( 𝑧 = → ( ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ) )
14 13 raleqbi1dv ( 𝑧 = → ( ∀ 𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑤 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) ) )
15 14 cbvralvw ( ∀ 𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑥𝑤 ∃! 𝑣𝑢𝑦 ( 𝑢𝑣𝑢 ) )
16 elequ1 ( 𝑤 = → ( 𝑤𝑢𝑢 ) )
17 16 anbi1d ( 𝑤 = → ( ( 𝑤𝑢𝑧𝑢 ) ↔ ( 𝑢𝑧𝑢 ) ) )
18 17 rexbidv ( 𝑤 = → ( ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃ 𝑢𝑦 ( 𝑢𝑧𝑢 ) ) )
19 18 reueqd ( 𝑤 = → ( ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) ) )
20 19 raleqbi1dv ( 𝑤 = → ( ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑡 ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) ) )
21 20 cbvralvw ( ∀ 𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑥𝑡 ∃! 𝑧𝑢𝑦 ( 𝑢𝑧𝑢 ) )
22 9 15 21 3bitr4i ( ∀ 𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∀ 𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) )
23 22 exbii ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) )
24 19.21v ( ∀ 𝑧 ( 𝑤𝑥 → ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤𝑥 → ∀ 𝑧 ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
25 impexp ( ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑧𝑤 → ( 𝑤𝑥 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
26 bi2.04 ( ( 𝑧𝑤 → ( 𝑤𝑥 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) ↔ ( 𝑤𝑥 → ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
27 25 26 bitri ( ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤𝑥 → ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
28 27 albii ( ∀ 𝑧 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑧 ( 𝑤𝑥 → ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
29 eu6 ( ∃! 𝑧 ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ ∃ 𝑥𝑧 ( ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
30 df-reu ( ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃! 𝑧 ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
31 19.42v ( ∃ 𝑥 ( 𝑧𝑤 ∧ ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) ↔ ( 𝑧𝑤 ∧ ∃ 𝑥 ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
32 an42 ( ( ( 𝑧𝑤𝑥𝑦 ) ∧ ( 𝑤𝑥𝑧𝑥 ) ) ↔ ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) )
33 anass ( ( ( 𝑧𝑤𝑥𝑦 ) ∧ ( 𝑤𝑥𝑧𝑥 ) ) ↔ ( 𝑧𝑤 ∧ ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
34 32 33 bitr3i ( ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ ( 𝑧𝑤 ∧ ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
35 34 exbii ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ ∃ 𝑥 ( 𝑧𝑤 ∧ ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
36 df-rex ( ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃ 𝑢 ( 𝑢𝑦 ∧ ( 𝑤𝑢𝑧𝑢 ) ) )
37 elequ1 ( 𝑢 = 𝑥 → ( 𝑢𝑦𝑥𝑦 ) )
38 elequ2 ( 𝑢 = 𝑥 → ( 𝑤𝑢𝑤𝑥 ) )
39 elequ2 ( 𝑢 = 𝑥 → ( 𝑧𝑢𝑧𝑥 ) )
40 38 39 anbi12d ( 𝑢 = 𝑥 → ( ( 𝑤𝑢𝑧𝑢 ) ↔ ( 𝑤𝑥𝑧𝑥 ) ) )
41 37 40 anbi12d ( 𝑢 = 𝑥 → ( ( 𝑢𝑦 ∧ ( 𝑤𝑢𝑧𝑢 ) ) ↔ ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
42 41 cbvexvw ( ∃ 𝑢 ( 𝑢𝑦 ∧ ( 𝑤𝑢𝑧𝑢 ) ) ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) )
43 36 42 bitri ( ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃ 𝑥 ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) )
44 43 anbi2i ( ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ ( 𝑧𝑤 ∧ ∃ 𝑥 ( 𝑥𝑦 ∧ ( 𝑤𝑥𝑧𝑥 ) ) ) )
45 31 35 44 3bitr4i ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
46 45 bibi1i ( ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ( ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
47 46 albii ( ∀ 𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∀ 𝑧 ( ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
48 47 exbii ( ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ↔ ∃ 𝑥𝑧 ( ( 𝑧𝑤 ∧ ∃ 𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ 𝑧 = 𝑥 ) )
49 29 30 48 3bitr4i ( ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
50 49 imbi2i ( ( 𝑡𝑤 → ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ ( 𝑡𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
51 50 albii ( ∀ 𝑡 ( 𝑡𝑤 → ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ ∀ 𝑡 ( 𝑡𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
52 df-ral ( ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑡 ( 𝑡𝑤 → ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
53 nfv 𝑡 ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
54 nfv 𝑧 𝑡𝑤
55 nfa1 𝑧𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 )
56 55 nfex 𝑧𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 )
57 54 56 nfim 𝑧 ( 𝑡𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) )
58 elequ1 ( 𝑧 = 𝑡 → ( 𝑧𝑤𝑡𝑤 ) )
59 58 imbi1d ( 𝑧 = 𝑡 → ( ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑡𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
60 53 57 59 cbvalv1 ( ∀ 𝑧 ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑡 ( 𝑡𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
61 51 52 60 3bitr4i ( ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑧 ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
62 61 imbi2i ( ( 𝑤𝑥 → ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) ↔ ( 𝑤𝑥 → ∀ 𝑧 ( 𝑧𝑤 → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ) )
63 24 28 62 3bitr4i ( ∀ 𝑧 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ( 𝑤𝑥 → ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
64 63 albii ( ∀ 𝑤𝑧 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤 ( 𝑤𝑥 → ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
65 alcom ( ∀ 𝑧𝑤 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) ↔ ∀ 𝑤𝑧 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
66 df-ral ( ∀ 𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑤 ( 𝑤𝑥 → ∀ 𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ) )
67 64 65 66 3bitr4ri ( ∀ 𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∀ 𝑧𝑤 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
68 67 exbii ( ∃ 𝑦𝑤𝑥𝑡𝑤 ∃! 𝑧𝑤𝑢𝑦 ( 𝑤𝑢𝑧𝑢 ) ↔ ∃ 𝑦𝑧𝑤 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )
69 23 68 bitri ( ∃ 𝑦𝑧𝑥𝑤𝑧 ∃! 𝑣𝑧𝑢𝑦 ( 𝑧𝑢𝑣𝑢 ) ↔ ∃ 𝑦𝑧𝑤 ( ( 𝑧𝑤𝑤𝑥 ) → ∃ 𝑥𝑧 ( ∃ 𝑥 ( ( 𝑧𝑤𝑤𝑥 ) ∧ ( 𝑧𝑥𝑥𝑦 ) ) ↔ 𝑧 = 𝑥 ) ) )