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

Metamath Proof Explorer

Theorem fsnd

Description: A singleton of an ordered pair is a function. (Contributed by AV, 17-Apr-2021)

Ref Expression
Hypotheses fsnd.a ⊢ φ → A ∈ V
fsnd.b ⊢ φ → B ∈ W
Assertion fsnd ⊢ φ → A B : A ⟶ W

Proof

Step Hyp Ref Expression
1 fsnd.a ⊢ φ → A ∈ V
2 fsnd.b ⊢ φ → B ∈ W
3 1 2 jca ⊢ φ → A ∈ V ∧ B ∈ W
4 f1sng ⊢ A ∈ V ∧ B ∈ W → A B : A ⟶ 1-1 W
5 f1f ⊢ A B : A ⟶ 1-1 W → A B : A ⟶ W
6 3 4 5 3syl ⊢ φ → A B : A ⟶ W