Theorem mptssid

Description: The mapping operation expressed with its actual domain. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	mptssid.1	⊢ Ⅎ 𝑥 𝐴
	mptssid.2	⊢ 𝐶 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
Assertion	mptssid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		mptssid.1	⊢ Ⅎ 𝑥 𝐴
2		mptssid.2	⊢ 𝐶 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V }
3		eqvisset	⊢ ( 𝑦 = 𝐵 → 𝐵 ∈ V )
4	3	anim2i	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) )
5		rabid	⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ↔ ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ V ) )
6	4 5	sylibr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } )
7	6 2	eleqtrrdi	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑥 ∈ 𝐶 )
8		simpr	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → 𝑦 = 𝐵 )
9	7 8	jca	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) )
10	1	ssrab2f	⊢ { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } ⊆ 𝐴
11	2 10	eqsstri	⊢ 𝐶 ⊆ 𝐴
12	11	sseli	⊢ ( 𝑥 ∈ 𝐶 → 𝑥 ∈ 𝐴 )
13	12	anim1i	⊢ ( ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) )
14	9 13	impbii	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) ↔ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) )
15	14	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) }
16		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
17		df-mpt	⊢ ( 𝑥 ∈ 𝐶 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐵 ) }
18	15 16 17	3eqtr4i	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )