This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Functions in maps-to notation mpteq2dva
Description: Slightly more general equality inference for the maps-to notation.
(Contributed by Scott Fenton , 25-Apr-2012) Remove dependency on
ax-10 . (Revised by SN , 11-Nov-2024)
Ref
Expression
Hypothesis
mpteq2dva.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
Assertion
mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
mpteq2dva.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐶 )
2
eqidd ⊢ ( 𝜑 → 𝐴 = 𝐴 )
3
2 1
mpteq12dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )