f1imaeq

Description: Taking images under a one-to-one function preserves equality. (Contributed by Stefan O'Rear, 30-Oct-2014)

		Ref	Expression
	Assertion	f1imaeq	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] = F [D] \leftrightarrow C = D)$

Step	Hyp	Ref	Expression
1		f1imass	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] \subseteq F [D] \leftrightarrow C \subseteq D)$
2		f1imass	$⊢ (F : A \underset{1-1}{⟶} B \land (D \subseteq A \land C \subseteq A)) \to (F [D] \subseteq F [C] \leftrightarrow D \subseteq C)$
3	2	ancom2s	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [D] \subseteq F [C] \leftrightarrow D \subseteq C)$
4	1 3	anbi12d	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to ((F [C] \subseteq F [D] \land F [D] \subseteq F [C]) \leftrightarrow (C \subseteq D \land D \subseteq C))$
5		eqss	$⊢ F [C] = F [D] \leftrightarrow (F [C] \subseteq F [D] \land F [D] \subseteq F [C])$
6		eqss	$⊢ C = D \leftrightarrow (C \subseteq D \land D \subseteq C)$
7	4 5 6	3bitr4g	$⊢ (F : A \underset{1-1}{⟶} B \land (C \subseteq A \land D \subseteq A)) \to (F [C] = F [D] \leftrightarrow C = D)$

Metamath Proof Explorer