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

Metamath Proof Explorer

Theorem funmpt2

Description: Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008) (Revised by Mario Carneiro, 31-May-2014)

Ref Expression
Hypothesis funmpt2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion funmpt2 Fun 𝐹

Proof

Step Hyp Ref Expression
1 funmpt2.1 ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2 funmpt ⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3 1 funeqi ⊢ ( Fun 𝐹 ↔ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
4 2 3 mpbir ⊢ Fun 𝐹