fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

		Ref	Expression
	Assertion	fvimacnvi	$⊢ (Fun F \land A \in F^{-1} [B]) \to F (A) \in B$

Step	Hyp	Ref	Expression
1		snssi	$⊢ A \in F^{-1} [B] \to \{A\} \subseteq F^{-1} [B]$
2		funimass2	$⊢ (Fun F \land \{A\} \subseteq F^{-1} [B]) \to F [\{A\}] \subseteq B$
3	1 2	sylan2	$⊢ (Fun F \land A \in F^{-1} [B]) \to F [\{A\}] \subseteq B$
4		fvex	$⊢ F (A) \in V$
5	4	snss	$⊢ F (A) \in B \leftrightarrow \{F (A)\} \subseteq B$
6		cnvimass	$⊢ F^{-1} [B] \subseteq dom F$
7	6	sseli	$⊢ A \in F^{-1} [B] \to A \in dom F$
8		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
9		fnsnfv	$⊢ (F Fn dom F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
10	8 9	sylanb	$⊢ (Fun F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
11	7 10	sylan2	$⊢ (Fun F \land A \in F^{-1} [B]) \to \{F (A)\} = F [\{A\}]$
12	11	sseq1d	$⊢ (Fun F \land A \in F^{-1} [B]) \to (\{F (A)\} \subseteq B \leftrightarrow F [\{A\}] \subseteq B)$
13	5 12	bitrid	$⊢ (Fun F \land A \in F^{-1} [B]) \to (F (A) \in B \leftrightarrow F [\{A\}] \subseteq B)$
14	3 13	mpbird	$⊢ (Fun F \land A \in F^{-1} [B]) \to F (A) \in B$

Metamath Proof Explorer