Theorem pmex

Description: The class of all partial functions from one set to another is a set. (Contributed by NM, 15-Nov-2007)

	Ref	Expression
Assertion	pmex	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐴 × 𝐵 ) ) } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		ancom	⊢ ( ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐴 × 𝐵 ) ) ↔ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) ∧ Fun 𝑓 ) )
2	1	abbii	⊢ { 𝑓 ∣ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐴 × 𝐵 ) ) } = { 𝑓 ∣ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) ∧ Fun 𝑓 ) }
3		xpexg	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 × 𝐵 ) ∈ V )
4		abssexg	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → { 𝑓 ∣ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) ∧ Fun 𝑓 ) } ∈ V )
5	3 4	syl	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( 𝑓 ⊆ ( 𝐴 × 𝐵 ) ∧ Fun 𝑓 ) } ∈ V )
6	2 5	eqeltrid	⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → { 𝑓 ∣ ( Fun 𝑓 ∧ 𝑓 ⊆ ( 𝐴 × 𝐵 ) ) } ∈ V )