This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐵 )