Theorem dmmptdf

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	dmmptdf.x	⊢ Ⅎ 𝑥 𝜑
	dmmptdf.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
	dmmptdf.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
Assertion	dmmptdf	⊢ ( 𝜑 → dom 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		dmmptdf.x	⊢ Ⅎ 𝑥 𝜑
2		dmmptdf.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
3		dmmptdf.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
4		nfcv	⊢ Ⅎ 𝑥 𝐵
5	1 4 2 3	dmmptdff	⊢ ( 𝜑 → dom 𝐴 = 𝐵 )