This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funfv1st2nd

Description: The function value for the first component of an ordered pair is the second component of the ordered pair. (Contributed by AV, 17-Oct-2023)

		Ref	Expression
	Assertion	funfv1st2nd	$⊢ (Fun F \land X \in F) \to F (1^{st} (X)) = 2^{nd} (X)$

Proof

Step	Hyp	Ref	Expression
1		funrel	$⊢ Fun F \to Rel F$
2		1st2nd	$⊢ (Rel F \land X \in F) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
3	1 2	sylan	$⊢ (Fun F \land X \in F) \to X = ⟨1^{st} (X), 2^{nd} (X)⟩$
4		eleq1	$⊢ X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to (X \in F \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in F)$
5	4	adantl	$⊢ (Fun F \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (X \in F \leftrightarrow ⟨1^{st} (X), 2^{nd} (X)⟩ \in F)$
6		funopfv	$⊢ Fun F \to (⟨1^{st} (X), 2^{nd} (X)⟩ \in F \to F (1^{st} (X)) = 2^{nd} (X))$
7	6	adantr	$⊢ (Fun F \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (⟨1^{st} (X), 2^{nd} (X)⟩ \in F \to F (1^{st} (X)) = 2^{nd} (X))$
8	5 7	sylbid	$⊢ (Fun F \land X = ⟨1^{st} (X), 2^{nd} (X)⟩) \to (X \in F \to F (1^{st} (X)) = 2^{nd} (X))$
9	8	impancom	$⊢ (Fun F \land X \in F) \to (X = ⟨1^{st} (X), 2^{nd} (X)⟩ \to F (1^{st} (X)) = 2^{nd} (X))$
10	3 9	mpd	$⊢ (Fun F \land X \in F) \to F (1^{st} (X)) = 2^{nd} (X)$