Step |
Hyp |
Ref |
Expression |
1 |
|
n0 |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ) |
2 |
|
elopab |
⊢ ( 𝑧 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
3 |
2
|
exbii |
⊢ ( ∃ 𝑧 𝑧 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
4 |
|
exrot3 |
⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
5 |
|
opex |
⊢ 〈 𝑥 , 𝑦 〉 ∈ V |
6 |
5
|
isseti |
⊢ ∃ 𝑧 𝑧 = 〈 𝑥 , 𝑦 〉 |
7 |
|
19.41v |
⊢ ( ∃ 𝑧 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ( ∃ 𝑧 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ) |
8 |
6 7
|
mpbiran |
⊢ ( ∃ 𝑧 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ 𝜑 ) |
9 |
8
|
2exbii |
⊢ ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) |
10 |
4 9
|
bitri |
⊢ ( ∃ 𝑧 ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) |
11 |
3 10
|
bitri |
⊢ ( ∃ 𝑧 𝑧 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) |
12 |
1 11
|
bitri |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 ∃ 𝑦 𝜑 ) |