imain

Description: The image of an intersection is the intersection of images. (Contributed by Paul Chapman, 11-Apr-2009)

		Ref	Expression
	Assertion	imain	$⊢ Fun F^{-1} \to F [A \cap B] = F [A] \cap F [B]$

Step	Hyp	Ref	Expression
1		imadif	$⊢ Fun F^{-1} \to F [A ∖ (A ∖ B)] = F [A] ∖ F [A ∖ B]$
2		imadif	$⊢ Fun F^{-1} \to F [A ∖ B] = F [A] ∖ F [B]$
3	2	difeq2d	$⊢ Fun F^{-1} \to F [A] ∖ F [A ∖ B] = F [A] ∖ (F [A] ∖ F [B])$
4	1 3	eqtrd	$⊢ Fun F^{-1} \to F [A ∖ (A ∖ B)] = F [A] ∖ (F [A] ∖ F [B])$
5		dfin4	$⊢ A \cap B = A ∖ (A ∖ B)$
6	5	imaeq2i	$⊢ F [A \cap B] = F [A ∖ (A ∖ B)]$
7		dfin4	$⊢ F [A] \cap F [B] = F [A] ∖ (F [A] ∖ F [B])$
8	4 6 7	3eqtr4g	$⊢ Fun F^{-1} \to F [A \cap B] = F [A] \cap F [B]$

Metamath Proof Explorer