Metamath Proof Explorer


Theorem oprabid

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker oprabidw when possible. (Contributed by Mario Carneiro, 20-Mar-2013) (New usage is discouraged.)

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

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 nfcvf2 ( ¬ ∀ 𝑥 𝑥 = 𝑧 𝑧 𝑥 )
38 nfcvd ( ¬ ∀ 𝑥 𝑥 = 𝑧 𝑧 𝑟 )
39 37 38 nfeqd ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑧 𝑥 = 𝑟 )
40 39 exdistrf ( ∃ 𝑥𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
41 40 eximi ( ∃ 𝑦𝑥𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑦𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
42 excom ( ∃ 𝑥𝑦𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) ↔ ∃ 𝑦𝑥𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
43 excom ( ∃ 𝑥𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) ↔ ∃ 𝑦𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
44 41 42 43 3imtr4i ( ∃ 𝑥𝑦𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑥𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
45 nfcvf2 ( ¬ ∀ 𝑥 𝑥 = 𝑦 𝑦 𝑥 )
46 nfcvd ( ¬ ∀ 𝑥 𝑥 = 𝑦 𝑦 𝑟 )
47 45 46 nfeqd ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑦 𝑥 = 𝑟 )
48 47 exdistrf ( ∃ 𝑥𝑦 ( 𝑥 = 𝑟 ∧ ∃ 𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) )
49 nfcvf2 ( ¬ ∀ 𝑦 𝑦 = 𝑧 𝑧 𝑦 )
50 nfcvd ( ¬ ∀ 𝑦 𝑦 = 𝑧 𝑧 𝑠 )
51 49 50 nfeqd ( ¬ ∀ 𝑦 𝑦 = 𝑧 → Ⅎ 𝑧 𝑦 = 𝑠 )
52 51 exdistrf ( ∃ 𝑦𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) → ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡𝜑 ) ) )
53 52 anim2i ( ( 𝑥 = 𝑟 ∧ ∃ 𝑦𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡𝜑 ) ) ) )
54 53 eximi ( ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦𝑧 ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡𝜑 ) ) ) )
55 44 48 54 3syl ( ∃ 𝑥𝑦𝑧 ( 𝑥 = 𝑟 ∧ ( 𝑦 = 𝑠 ∧ ( 𝑧 = 𝑡𝜑 ) ) ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡𝜑 ) ) ) )
56 36 55 sylbi ( ∃ 𝑥𝑦𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑟 ∧ ∃ 𝑦 ( 𝑦 = 𝑠 ∧ ∃ 𝑧 ( 𝑧 = 𝑡𝜑 ) ) ) )
57 29 56 syl11 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥𝑦𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) )
58 eqeq1 ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
59 eqcom ( ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ )
60 58 59 bitrdi ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ) )
61 60 anbi1d ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ) )
62 61 3exbidv ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥𝑦𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) ) )
63 62 imbi1d ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ↔ ( ∃ 𝑥𝑦𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
64 60 63 imbi12d ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ↔ ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( ∃ 𝑥𝑦𝑧 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
65 57 64 mpbiri ( 𝑤 = ⟨ ⟨ 𝑟 , 𝑠 ⟩ , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
66 15 65 syl6bi ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
67 66 adantr ( ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
68 67 exlimivv ( ∃ 𝑟𝑠 ( 𝑎 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ⟨ 𝑟 , 𝑠 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
69 13 68 sylbi ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
70 69 com3l ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝑎 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) ) )
71 10 70 mpdd ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
72 71 adantr ( ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
73 72 exlimivv ( ∃ 𝑎𝑡 ( 𝑤 = ⟨ 𝑎 , 𝑡 ⟩ ∧ ⟨ 𝑎 , 𝑡 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) → ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) ) )
74 5 73 mpcom ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → 𝜑 ) )
75 19.8a ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
76 19.8a ( ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
77 19.8a ( ∃ 𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
78 75 76 77 3syl ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) → ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) )
79 78 ex ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 → ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ) )
80 74 79 impbid ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) ↔ 𝜑 ) )
81 df-oprab { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } = { 𝑤 ∣ ∃ 𝑥𝑦𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ 𝜑 ) }
82 1 80 81 elab2 ( ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ 𝜑 } ↔ 𝜑 )