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

Metamath Proof Explorer

Theorem fsetex

Description: The set of functions between two classes exists if the codomain exists. Generalization of mapex to arbitrary domains. (Contributed by AV, 14-Aug-2024)

		Ref	Expression
	Assertion	fsetex	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		mapfset	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } = ( 𝐵 ↑_m 𝐴 ) )
2		ovex	⊢ ( 𝐵 ↑_m 𝐴 ) ∈ V
3	1 2	eqeltrdi	⊢ ( 𝐵 ∈ 𝑉 → { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } ∈ V )