Theorem dmmptdff

Description: The domain of the mapping operation, deduction form. (Contributed by Glauco Siliprandi, 21-Dec-2024)

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

Proof

Step	Hyp	Ref	Expression
1		dmmptdff.x	⊢ Ⅎ 𝑥 𝜑
2		dmmptdff.1	⊢ Ⅎ 𝑥 𝐵
3		dmmptdff.a	⊢ 𝐴 = ( 𝑥 ∈ 𝐵 ↦ 𝐶 )
4		dmmptdff.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝑉 )
5	3	dmmpt	⊢ dom 𝐴 = { 𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V }
6	4	elexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ V )
7	1 6	ralrimia	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 𝐶 ∈ V )
8	2	rabid2f	⊢ ( 𝐵 = { 𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V } ↔ ∀ 𝑥 ∈ 𝐵 𝐶 ∈ V )
9	7 8	sylibr	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ 𝐵 ∣ 𝐶 ∈ V } )
10	5 9	eqtr4id	⊢ ( 𝜑 → dom 𝐴 = 𝐵 )