Step |
Hyp |
Ref |
Expression |
1 |
|
ssun2 |
⊢ 𝐴 ⊆ ( 𝐵 ∪ 𝐴 ) |
2 |
|
undif2 |
⊢ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) = ( 𝐵 ∪ 𝐴 ) |
3 |
1 2
|
sseqtrri |
⊢ 𝐴 ⊆ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) |
4 |
|
imass2 |
⊢ ( 𝐴 ⊆ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) → ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) ) |
5 |
3 4
|
ax-mp |
⊢ ( 𝐹 “ 𝐴 ) ⊆ ( 𝐹 “ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) |
6 |
|
imaundi |
⊢ ( 𝐹 “ ( 𝐵 ∪ ( 𝐴 ∖ 𝐵 ) ) ) = ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) |
7 |
5 6
|
sseqtri |
⊢ ( 𝐹 “ 𝐴 ) ⊆ ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) |
8 |
|
ssundif |
⊢ ( ( 𝐹 “ 𝐴 ) ⊆ ( ( 𝐹 “ 𝐵 ) ∪ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) ↔ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) ) |
9 |
7 8
|
mpbi |
⊢ ( ( 𝐹 “ 𝐴 ) ∖ ( 𝐹 “ 𝐵 ) ) ⊆ ( 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) |