Proof of Theorem dfopab2
Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 2973 |
. . . . 5
⊢
Ⅎ𝑥[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 |
2 | 1 | 19.41 1679 |
. . . 4
⊢
(∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
3 | | sbcopeq1a 6166 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ([(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑 ↔ 𝜑)) |
4 | 3 | pm5.32i 451 |
. . . . . . 7
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
5 | 4 | exbii 1598 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
6 | | nfcv 2312 |
. . . . . . . 8
⊢
Ⅎ𝑦(1st ‘𝑧) |
7 | | nfsbc1v 2973 |
. . . . . . . 8
⊢
Ⅎ𝑦[(2nd ‘𝑧) / 𝑦]𝜑 |
8 | 6, 7 | nfsbc 2975 |
. . . . . . 7
⊢
Ⅎ𝑦[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 |
9 | 8 | 19.41 1679 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
10 | 5, 9 | bitr3i 185 |
. . . . 5
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
11 | 10 | exbii 1598 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
12 | | elvv 4673 |
. . . . 5
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉) |
13 | 12 | anbi1i 455 |
. . . 4
⊢ ((𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
14 | 2, 11, 13 | 3bitr4i 211 |
. . 3
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)) |
15 | 14 | abbii 2286 |
. 2
⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} = {𝑧 ∣ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)} |
16 | | df-opab 4051 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
17 | | df-rab 2457 |
. 2
⊢ {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} = {𝑧 ∣ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)} |
18 | 15, 16, 17 | 3eqtr4i 2201 |
1
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} |