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

Metamath Proof Explorer

Theorem fex2

Description: A function with bounded domain and codomain 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 )