elpreima

Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	elpreima	$⊢ F Fn A \to (B \in F^{-1} [C] \leftrightarrow (B \in A \land F (B) \in C))$

Step	Hyp	Ref	Expression
1		cnvimass	$⊢ F^{-1} [C] \subseteq dom F$
2	1	sseli	$⊢ B \in F^{-1} [C] \to B \in dom F$
3		fndm	$⊢ F Fn A \to dom F = A$
4	3	eleq2d	$⊢ F Fn A \to (B \in dom F \leftrightarrow B \in A)$
5	2 4	imbitrid	$⊢ F Fn A \to (B \in F^{-1} [C] \to B \in A)$
6		fnfun	$⊢ F Fn A \to Fun F$
7		fvimacnvi	$⊢ (Fun F \land B \in F^{-1} [C]) \to F (B) \in C$
8	6 7	sylan	$⊢ (F Fn A \land B \in F^{-1} [C]) \to F (B) \in C$
9	8	ex	$⊢ F Fn A \to (B \in F^{-1} [C] \to F (B) \in C)$
10	5 9	jcad	$⊢ F Fn A \to (B \in F^{-1} [C] \to (B \in A \land F (B) \in C))$
11		fvimacnv	$⊢ (Fun F \land B \in dom F) \to (F (B) \in C \leftrightarrow B \in F^{-1} [C])$
12	11	funfni	$⊢ (F Fn A \land B \in A) \to (F (B) \in C \leftrightarrow B \in F^{-1} [C])$
13	12	biimpd	$⊢ (F Fn A \land B \in A) \to (F (B) \in C \to B \in F^{-1} [C])$
14	13	expimpd	$⊢ F Fn A \to ((B \in A \land F (B) \in C) \to B \in F^{-1} [C])$
15	10 14	impbid	$⊢ F Fn A \to (B \in F^{-1} [C] \leftrightarrow (B \in A \land F (B) \in C))$

Metamath Proof Explorer