Step |
Hyp |
Ref |
Expression |
1 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } |
2 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } |
3 |
1 2
|
uneq12i |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) |
4 |
|
df-rab |
⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∨ 𝜓 ) ) } |
5 |
|
unab |
⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) } |
6 |
|
andi |
⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∨ 𝜓 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) ) |
7 |
6
|
abbii |
⊢ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∨ 𝜓 ) ) } = { 𝑥 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ∨ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) ) } |
8 |
5 7
|
eqtr4i |
⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ ( 𝜑 ∨ 𝜓 ) ) } |
9 |
4 8
|
eqtr4i |
⊢ { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } = ( { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) } ∪ { 𝑥 ∣ ( 𝑥 ∈ 𝐴 ∧ 𝜓 ) } ) |
10 |
3 9
|
eqtr4i |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐴 ∣ 𝜓 } ) = { 𝑥 ∈ 𝐴 ∣ ( 𝜑 ∨ 𝜓 ) } |