Metamath Proof Explorer


Theorem fex2

Description: A function with bounded domain and range is a set. This version of fex is proven without the Axiom of Replacement ax-rep , but depends on ax-un , which is not required for the proof of fex . (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Assertion fex2 ( ( 𝐹 : 𝐴𝐵𝐴𝑉𝐵𝑊 ) → 𝐹 ∈ V )

Proof

Step Hyp Ref Expression
1 xpexg ( ( 𝐴𝑉𝐵𝑊 ) → ( 𝐴 × 𝐵 ) ∈ V )
2 1 3adant1 ( ( 𝐹 : 𝐴𝐵𝐴𝑉𝐵𝑊 ) → ( 𝐴 × 𝐵 ) ∈ V )
3 fssxp ( 𝐹 : 𝐴𝐵𝐹 ⊆ ( 𝐴 × 𝐵 ) )
4 3 3ad2ant1 ( ( 𝐹 : 𝐴𝐵𝐴𝑉𝐵𝑊 ) → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
5 2 4 ssexd ( ( 𝐹 : 𝐴𝐵𝐴𝑉𝐵𝑊 ) → 𝐹 ∈ V )