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

Metamath Proof Explorer

Theorem mapex

Description: The class of all functions mapping one set to another is a set. Remark after Definition 10.24 of Kunen p. 31. (Contributed by Raph Levien, 4-Dec-2003) (Proof shortened by AV, 16-Jun-2025)

Ref Expression
Assertion mapex ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ B ∈ V

Proof

Step Hyp Ref Expression
1 eqid ⊢ f | f : A ⟶ B ∧ f : A ⟶ B = f | f : A ⟶ B ∧ f : A ⟶ B
2 1 fabexg ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ B ∧ f : A ⟶ B ∈ V
3 id ⊢ f : A ⟶ B → f : A ⟶ B
4 3 ancli ⊢ f : A ⟶ B → f : A ⟶ B ∧ f : A ⟶ B
5 4 ss2abi ⊢ f | f : A ⟶ B ⊆ f | f : A ⟶ B ∧ f : A ⟶ B
6 5 a1i ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ B ⊆ f | f : A ⟶ B ∧ f : A ⟶ B
7 2 6 ssexd ⊢ A ∈ C ∧ B ∈ D → f | f : A ⟶ B ∈ V