Metamath Proof Explorer

Theorem funfvima3

Description: A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004)

		Ref	Expression
	Assertion	funfvima3	$⊢ (Fun F \land F \subseteq G) \to (A \in dom F \to F (A) \in G [\{A\}])$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ F \subseteq G \to (⟨A, F (A)⟩ \in F \to ⟨A, F (A)⟩ \in G)$
2		funfvop	$⊢ (Fun F \land A \in dom F) \to ⟨A, F (A)⟩ \in F$
3	1 2	impel	$⊢ (F \subseteq G \land (Fun F \land A \in dom F)) \to ⟨A, F (A)⟩ \in G$
4		sneq	$⊢ x = A \to \{x\} = \{A\}$
5	4	imaeq2d	$⊢ x = A \to G [\{x\}] = G [\{A\}]$
6	5	eleq2d	$⊢ x = A \to (F (A) \in G [\{x\}] \leftrightarrow F (A) \in G [\{A\}])$
7		opeq1	$⊢ x = A \to ⟨x, F (A)⟩ = ⟨A, F (A)⟩$
8	7	eleq1d	$⊢ x = A \to (⟨x, F (A)⟩ \in G \leftrightarrow ⟨A, F (A)⟩ \in G)$
9		vex	$⊢ x \in V$
10		fvex	$⊢ F (A) \in V$
11	9 10	elimasn	$⊢ F (A) \in G [\{x\}] \leftrightarrow ⟨x, F (A)⟩ \in G$
12	6 8 11	vtoclbg	$⊢ A \in dom F \to (F (A) \in G [\{A\}] \leftrightarrow ⟨A, F (A)⟩ \in G)$
13	12	ad2antll	$⊢ (F \subseteq G \land (Fun F \land A \in dom F)) \to (F (A) \in G [\{A\}] \leftrightarrow ⟨A, F (A)⟩ \in G)$
14	3 13	mpbird	$⊢ (F \subseteq G \land (Fun F \land A \in dom F)) \to F (A) \in G [\{A\}]$
15	14	exp32	$⊢ F \subseteq G \to (Fun F \to (A \in dom F \to F (A) \in G [\{A\}]))$
16	15	impcom	$⊢ (Fun F \land F \subseteq G) \to (A \in dom F \to F (A) \in G [\{A\}])$