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 bitrdi ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ) )
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 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )