Metamath Proof Explorer

Theorem oprabidw

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Version of oprabid with a disjoint variable condition, which does not require ax-13 . (Contributed by Mario Carneiro, 20-Mar-2013) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Assertion oprabidw ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )

Proof

Step Hyp Ref Expression
1 opex ⊢ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ V
2 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
3 vex ⊢ 𝑧 ∈ V
4 2 3 eqvinop ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ∃ 𝑎 ∃ 𝑡 ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
5 4 biimpi ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ∃ 𝑎 ∃ 𝑡 ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
6 eqeq1 ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
7 vex ⊢ 𝑎 ∈ V
8 vex ⊢ 𝑡 ∈ V
9 7 8 opth1 ⊢ ( ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ )
10 6 9 syl6bi ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ) )
11 vex ⊢ 𝑥 ∈ V
12 vex ⊢ 𝑦 ∈ V
13 11 12 eqvinop ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑟 ∃ 𝑠 ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
14 opeq1 ⊢ ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ → ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ )
15 14 eqeq2d ⊢ ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ↔ 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ) )
16 11 12 3 otth2 ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ↔ ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡 ) )
17 euequ ⊢ ∃! 𝑥 𝑥 = 𝑟
18 eupick ⊢ ( ( ∃! 𝑥 𝑥 = 𝑟 ∧ ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) → ( 𝑥 = 𝑟 → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
19 17 18 mpan ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
20 euequ ⊢ ∃! 𝑦 𝑦 = 𝑠
21 eupick ⊢ ( ( ∃! 𝑦 𝑦 = 𝑠 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑦 = 𝑠 → ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
22 20 21 mpan ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( 𝑦 = 𝑠 → ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
23 euequ ⊢ ∃! 𝑧 𝑧 = 𝑡
24 eupick ⊢ ( ( ∃! 𝑧 𝑧 = 𝑡 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( 𝑧 = 𝑡 → 𝜑 ) )
25 23 24 mpan ⊢ ( ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) → ( 𝑧 = 𝑡 → 𝜑 ) )
26 22 25 syl6 ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( 𝑦 = 𝑠 → ( 𝑧 = 𝑡 → 𝜑 ) ) )
27 19 26 syl6 ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 → ( 𝑦 = 𝑠 → ( 𝑧 = 𝑡 → 𝜑 ) ) ) )
28 27 3impd ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡 ) → 𝜑 ) )
29 16 28 syl5bi ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → 𝜑 ) )
30 df-3an ⊢ ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ∧ 𝑧 = 𝑡 ) ↔ ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ 𝑧 = 𝑡 ) )
31 16 30 bitri ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ↔ ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ 𝑧 = 𝑡 ) )
32 31 anbi1i ⊢ ( ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ↔ ( ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ 𝑧 = 𝑡 ) ∧ 𝜑 ) )
33 anass ⊢ ( ( ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ 𝑧 = 𝑡 ) ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
34 anass ⊢ ( ( ( 𝑥 = 𝑟 ∧ 𝑦 = 𝑠 ) ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ↔ ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
35 32 33 34 3bitri ⊢ ( ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ↔ ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
36 35 3exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
37 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
38 19.8a ⊢ ( ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
39 38 anim2i ⊢ ( ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
40 39 eximi ⊢ ( ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
41 biidd ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
42 41 drex1v ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
43 40 42 syl5ibr ⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
44 19.40 ⊢ ( ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( ∃ 𝑧 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
45 nfvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑥 = 𝑟 )
46 45 19.9d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑧 𝑥 = 𝑟 → 𝑥 = 𝑟 ) )
47 46 anim1d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ( ∃ 𝑧 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
48 19.8a ⊢ ( ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
49 44 47 48 syl56 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
50 43 49 pm2.61i ⊢ ( ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
51 37 50 exlimi ⊢ ( ∃ 𝑥 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
52 51 eximi ⊢ ( ∃ 𝑦 ∃ 𝑥 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
53 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ∃ 𝑦 ∃ 𝑥 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
54 excom ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
55 52 53 54 3imtr4i ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
56 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
57 19.8a ⊢ ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
58 57 anim2i ⊢ ( ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
59 58 eximi ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
60 biidd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
61 60 drex1v ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ↔ ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
62 59 61 syl5ibr ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
63 19.40 ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( ∃ 𝑦 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
64 nfvd ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑟 )
65 64 19.9d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 𝑥 = 𝑟 → 𝑥 = 𝑟 ) )
66 65 anim1d ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ( ∃ 𝑦 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
67 19.8a ⊢ ( ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
68 63 66 67 syl56 ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) ) )
69 62 68 pm2.61i ⊢ ( ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
70 56 69 exlimi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
71 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) )
72 19.8a ⊢ ( ( 𝑧 = 𝑡 ∧ 𝜑 ) → ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) )
73 72 anim2i ⊢ ( ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
74 73 eximi ⊢ ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
75 biidd ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ↔ ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
76 75 drex1v ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ↔ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
77 74 76 syl5ibr ⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
78 19.40 ⊢ ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( ∃ 𝑧 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
79 nfvd ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑦 = 𝑠 )
80 79 19.9d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑧 𝑦 = 𝑠 → 𝑦 = 𝑠 ) )
81 80 anim1d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ( ∃ 𝑧 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
82 19.8a ⊢ ( ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
83 78 81 82 syl56 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
84 77 83 pm2.61i ⊢ ( ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
85 71 84 exlimi ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) )
86 85 anim2i ⊢ ( ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
87 86 eximi ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
88 55 70 87 3syl ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
89 36 88 sylbi ⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡 ∧ 𝜑 ) ) ) )
90 29 89 syl11 ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) )
91 eqeq1 ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
92 eqcom ⊢ ( ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ )
93 91 92 syl6bb ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ) )
94 93 anbi1d ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ) )
95 94 3exbidv ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ) )
96 95 imbi1d ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
97 93 96 imbi12d ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ↔ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
98 90 97 mpbiri ⊢ ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
99 15 98 syl6bi ⊢ ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
100 99 adantr ⊢ ( ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
101 100 exlimivv ⊢ ( ∃ 𝑟 ∃ 𝑠 ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
102 13 101 sylbi ⊢ ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
103 102 com3l ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
104 10 103 mpdd ⊢ ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
105 104 adantr ⊢ ( ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
106 105 exlimivv ⊢ ( ∃ 𝑎 ∃ 𝑡 ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
107 5 106 mpcom ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) )
108 19.8a ⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
109 19.8a ⊢ ( ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
110 19.8a ⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
111 108 109 110 3syl ⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
112 111 ex ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
113 107 112 impbid ⊢ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ 𝜑 ) )
114 df-oprab ⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
115 1 113 114 elab2 ⊢ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )