Metamath Proof Explorer


Theorem mpteq12df

Description: An equality inference for the maps-to notation. Compare mpteq12dv . (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Hypotheses mpteq12df.1 𝑥 𝜑
mpteq12df.2 ( 𝜑𝐴 = 𝐶 )
mpteq12df.3 ( 𝜑𝐵 = 𝐷 )
Assertion mpteq12df ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐶𝐷 ) )

Proof

Step Hyp Ref Expression
1 mpteq12df.1 𝑥 𝜑
2 mpteq12df.2 ( 𝜑𝐴 = 𝐶 )
3 mpteq12df.3 ( 𝜑𝐵 = 𝐷 )
4 nfv 𝑦 𝜑
5 2 eleq2d ( 𝜑 → ( 𝑥𝐴𝑥𝐶 ) )
6 3 eqeq2d ( 𝜑 → ( 𝑦 = 𝐵𝑦 = 𝐷 ) )
7 5 6 anbi12d ( 𝜑 → ( ( 𝑥𝐴𝑦 = 𝐵 ) ↔ ( 𝑥𝐶𝑦 = 𝐷 ) ) )
8 1 4 7 opabbid ( 𝜑 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐵 ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦 = 𝐷 ) } )
9 df-mpt ( 𝑥𝐴𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = 𝐵 ) }
10 df-mpt ( 𝑥𝐶𝐷 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐶𝑦 = 𝐷 ) }
11 8 9 10 3eqtr4g ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐶𝐷 ) )