Proof of Theorem dfopab2
Step | Hyp | Ref
| Expression |
1 | | nfsbc1v 3737 |
. . . . 5
⊢
Ⅎ𝑥[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 |
2 | 1 | 19.41 2228 |
. . . 4
⊢
(∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑥∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
3 | | sbcopeq1a 7890 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ([(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑 ↔ 𝜑)) |
4 | 3 | pm5.32i 575 |
. . . . . . 7
⊢ ((𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
5 | 4 | exbii 1850 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ ∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)) |
6 | | nfcv 2907 |
. . . . . . . 8
⊢
Ⅎ𝑦(1st ‘𝑧) |
7 | | nfsbc1v 3737 |
. . . . . . . 8
⊢
Ⅎ𝑦[(2nd ‘𝑧) / 𝑦]𝜑 |
8 | 6, 7 | nfsbcw 3739 |
. . . . . . 7
⊢
Ⅎ𝑦[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑 |
9 | 8 | 19.41 2228 |
. . . . . 6
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
10 | 5, 9 | bitr3i 276 |
. . . . 5
⊢
(∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ (∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
11 | 10 | exbii 1850 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑) ↔ ∃𝑥(∃𝑦 𝑧 = 〈𝑥, 𝑦〉 ∧ [(1st
‘𝑧) / 𝑥][(2nd
‘𝑧) / 𝑦]𝜑)) |
12 | | elvv 5663 |
. . . . 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 5139 |
. 2
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜑)} |
17 | | df-rab 3073 |
. 2
⊢ {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} = {𝑧 ∣ (𝑧 ∈ (V × V) ∧
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑)} |
18 | 15, 16, 17 | 3eqtr4i 2776 |
1
⊢
{〈𝑥, 𝑦〉 ∣ 𝜑} = {𝑧 ∈ (V × V) ∣
[(1st ‘𝑧) / 𝑥][(2nd ‘𝑧) / 𝑦]𝜑} |