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 ( ( 𝐴𝐶𝐵𝐷 ) → { 𝑓𝑓 : 𝐴𝐵 } ∈ V )

Proof

Step Hyp Ref Expression
1 eqid { 𝑓 ∣ ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) } = { 𝑓 ∣ ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) }
2 1 fabexg ( ( 𝐴𝐶𝐵𝐷 ) → { 𝑓 ∣ ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) } ∈ V )
3 id ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 )
4 3 ancli ( 𝑓 : 𝐴𝐵 → ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) )
5 4 ss2abi { 𝑓𝑓 : 𝐴𝐵 } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) }
6 5 a1i ( ( 𝐴𝐶𝐵𝐷 ) → { 𝑓𝑓 : 𝐴𝐵 } ⊆ { 𝑓 ∣ ( 𝑓 : 𝐴𝐵𝑓 : 𝐴𝐵 ) } )
7 2 6 ssexd ( ( 𝐴𝐶𝐵𝐷 ) → { 𝑓𝑓 : 𝐴𝐵 } ∈ V )