Theorem elpm2g

Description: The predicate "is a partial function". (Contributed by NM, 31-Dec-2013)

	Ref	Expression
Assertion	elpm2g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elpmg	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐵 × 𝐴 ) ) ) )
2		funssxp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ ( 𝐵 × 𝐴 ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) )
3	1 2	bitrdi	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) ↔ ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) ) )