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