Step |
Hyp |
Ref |
Expression |
1 |
|
unab |
|- ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ -. ph ) } ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } |
2 |
|
df-rab |
|- { x e. A | ph } = { x | ( x e. A /\ ph ) } |
3 |
|
df-rab |
|- { x e. B | -. ph } = { x | ( x e. B /\ -. ph ) } |
4 |
2 3
|
uneq12i |
|- ( { x e. A | ph } u. { x e. B | -. ph } ) = ( { x | ( x e. A /\ ph ) } u. { x | ( x e. B /\ -. ph ) } ) |
5 |
|
df-if |
|- if ( ph , A , B ) = { x | ( ( x e. A /\ ph ) \/ ( x e. B /\ -. ph ) ) } |
6 |
1 4 5
|
3eqtr4ri |
|- if ( ph , A , B ) = ( { x e. A | ph } u. { x e. B | -. ph } ) |