This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Preimage of a difference. (Contributed by Mario Carneiro, 14-Jun-2016)
|
|
Ref |
Expression |
|
Assertion |
difpreima |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∖ ( ◡ 𝐹 “ 𝐵 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
funcnvcnv |
⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 ) |
| 2 |
|
imadif |
⊢ ( Fun ◡ ◡ 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∖ ( ◡ 𝐹 “ 𝐵 ) ) ) |
| 3 |
1 2
|
syl |
⊢ ( Fun 𝐹 → ( ◡ 𝐹 “ ( 𝐴 ∖ 𝐵 ) ) = ( ( ◡ 𝐹 “ 𝐴 ) ∖ ( ◡ 𝐹 “ 𝐵 ) ) ) |