Theorem dmmptg

Description: The domain of the mapping operation is the stated domain, if the function value is always a set. (Contributed by Mario Carneiro, 9-Feb-2013) (Revised by Mario Carneiro, 14-Sep-2013)

	Ref	Expression
Assertion	dmmptg	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	dmmpt	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
3		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
4	3	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
5		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
6	4 5	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } )
7	2 6	eqtr4id	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )