Proof of Theorem dfopab2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | nfsbc1v 3807 | . . . . 5
⊢
Ⅎ𝑥[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 | 
| 2 | 1 | 19.41 2234 | . . . 4
⊢
(∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) | 
| 3 |  | sbcopeq1a 8075 | . . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ([(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑 ↔ 𝜑)) | 
| 4 | 3 | pm5.32i 574 | . . . . . . 7
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) | 
| 5 | 4 | exbii 1847 | . . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) | 
| 6 |  | nfcv 2904 | . . . . . . . 8
⊢
Ⅎ𝑦(1st ‘𝑧) | 
| 7 |  | nfsbc1v 3807 | . . . . . . . 8
⊢
Ⅎ𝑦[(2nd ‘𝑧) / 𝑦]𝜑 | 
| 8 | 6, 7 | nfsbcw 3809 | . . . . . . 7
⊢
Ⅎ𝑦[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 | 
| 9 | 8 | 19.41 2234 | . . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) | 
| 10 | 5, 9 | bitr3i 277 | . . . . 5
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) | 
| 11 | 10 | exbii 1847 | . . . 4
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) | 
| 12 |  | elvv 5759 | . . . . 5
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) | 
| 13 | 12 | anbi1i 624 | . . . 4
⊢ ((𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) | 
| 14 | 2, 11, 13 | 3bitr4i 303 | . . 3
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)) | 
| 15 | 14 | abbii 2808 | . 2
⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)} | 
| 16 |  | df-opab 5205 | . 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} | 
| 17 |  | df-rab 3436 | . 2
⊢ {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} = {𝑧 ∣ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)} | 
| 18 | 15, 16, 17 | 3eqtr4i 2774 | 1
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} |