Step |
Hyp |
Ref |
Expression |
1 |
|
unab |
⊢ ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } ) = { 𝑧 ∣ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) } |
2 |
|
19.43 |
⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ) |
3 |
|
andi |
⊢ ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) ↔ ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ) |
4 |
3
|
exbii |
⊢ ( ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) ↔ ∃ 𝑦 ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ) |
5 |
|
19.43 |
⊢ ( ∃ 𝑦 ( ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ) |
6 |
4 5
|
bitr2i |
⊢ ( ( ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) ) |
7 |
6
|
exbii |
⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) ) |
8 |
2 7
|
bitr3i |
⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) ) |
9 |
8
|
abbii |
⊢ { 𝑧 ∣ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) } |
10 |
1 9
|
eqtri |
⊢ ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) } |
11 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } |
12 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } |
13 |
11 12
|
uneq12i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ∪ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) = ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ 𝜓 ) } ) |
14 |
|
df-opab |
⊢ { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = 〈 𝑥 , 𝑦 〉 ∧ ( 𝜑 ∨ 𝜓 ) ) } |
15 |
10 13 14
|
3eqtr4i |
⊢ ( { 〈 𝑥 , 𝑦 〉 ∣ 𝜑 } ∪ { 〈 𝑥 , 𝑦 〉 ∣ 𝜓 } ) = { 〈 𝑥 , 𝑦 〉 ∣ ( 𝜑 ∨ 𝜓 ) } |