fvelrn

Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996)

		Ref	Expression
	Assertion	fvelrn	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ x = A \to (x \in dom F \leftrightarrow A \in dom F)$
2	1	anbi2d	$⊢ x = A \to ((Fun F \land x \in dom F) \leftrightarrow (Fun F \land A \in dom F))$
3		fveq2	$⊢ x = A \to F (x) = F (A)$
4	3	eleq1d	$⊢ x = A \to (F (x) \in ran F \leftrightarrow F (A) \in ran F)$
5	2 4	imbi12d	$⊢ x = A \to (((Fun F \land x \in dom F) \to F (x) \in ran F) \leftrightarrow ((Fun F \land A \in dom F) \to F (A) \in ran F))$
6		funfvop	$⊢ (Fun F \land x \in dom F) \to ⟨x, F (x)⟩ \in F$
7		vex	$⊢ x \in V$
8		opeq1	$⊢ y = x \to ⟨y, F (x)⟩ = ⟨x, F (x)⟩$
9	8	eleq1d	$⊢ y = x \to (⟨y, F (x)⟩ \in F \leftrightarrow ⟨x, F (x)⟩ \in F)$
10	7 9	spcev	$⊢ ⟨x, F (x)⟩ \in F \to \exists y ⟨y, F (x)⟩ \in F$
11	6 10	syl	$⊢ (Fun F \land x \in dom F) \to \exists y ⟨y, F (x)⟩ \in F$
12		fvex	$⊢ F (x) \in V$
13	12	elrn2	$⊢ F (x) \in ran F \leftrightarrow \exists y ⟨y, F (x)⟩ \in F$
14	11 13	sylibr	$⊢ (Fun F \land x \in dom F) \to F (x) \in ran F$
15	5 14	vtoclg	$⊢ A \in dom F \to ((Fun F \land A \in dom F) \to F (A) \in ran F)$
16	15	anabsi7	$⊢ (Fun F \land A \in dom F) \to F (A) \in ran F$

Metamath Proof Explorer