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		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
2	1	ralimi	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
3		rabid2	⊢ ( 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ↔ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
4	2 3	sylibr	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → 𝐴 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } )
5		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6	5	dmmpt	⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
7	4 6	syl6reqr	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )