Step |
Hyp |
Ref |
Expression |
1 |
|
dfif3.1 |
⊢ 𝐶 = { 𝑥 ∣ 𝜑 } |
2 |
|
dfif6 |
⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑦 ∈ 𝐵 ∣ ¬ 𝜑 } ) |
3 |
|
biidd |
⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜑 ) ) |
4 |
3
|
cbvabv |
⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜑 } |
5 |
1 4
|
eqtri |
⊢ 𝐶 = { 𝑦 ∣ 𝜑 } |
6 |
5
|
ineq2i |
⊢ ( 𝐴 ∩ 𝐶 ) = ( 𝐴 ∩ { 𝑦 ∣ 𝜑 } ) |
7 |
|
dfrab3 |
⊢ { 𝑦 ∈ 𝐴 ∣ 𝜑 } = ( 𝐴 ∩ { 𝑦 ∣ 𝜑 } ) |
8 |
6 7
|
eqtr4i |
⊢ ( 𝐴 ∩ 𝐶 ) = { 𝑦 ∈ 𝐴 ∣ 𝜑 } |
9 |
|
dfrab3 |
⊢ { 𝑦 ∈ 𝐵 ∣ ¬ 𝜑 } = ( 𝐵 ∩ { 𝑦 ∣ ¬ 𝜑 } ) |
10 |
|
notab |
⊢ { 𝑦 ∣ ¬ 𝜑 } = ( V ∖ { 𝑦 ∣ 𝜑 } ) |
11 |
5
|
difeq2i |
⊢ ( V ∖ 𝐶 ) = ( V ∖ { 𝑦 ∣ 𝜑 } ) |
12 |
10 11
|
eqtr4i |
⊢ { 𝑦 ∣ ¬ 𝜑 } = ( V ∖ 𝐶 ) |
13 |
12
|
ineq2i |
⊢ ( 𝐵 ∩ { 𝑦 ∣ ¬ 𝜑 } ) = ( 𝐵 ∩ ( V ∖ 𝐶 ) ) |
14 |
9 13
|
eqtr2i |
⊢ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) = { 𝑦 ∈ 𝐵 ∣ ¬ 𝜑 } |
15 |
8 14
|
uneq12i |
⊢ ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) = ( { 𝑦 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑦 ∈ 𝐵 ∣ ¬ 𝜑 } ) |
16 |
2 15
|
eqtr4i |
⊢ if ( 𝜑 , 𝐴 , 𝐵 ) = ( ( 𝐴 ∩ 𝐶 ) ∪ ( 𝐵 ∩ ( V ∖ 𝐶 ) ) ) |