Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Functions in maps-to notation
mpteq12dvOLD
Metamath Proof Explorer
Description: Obsolete version of mpteq12dv as of 1-Dec-2023. (Contributed by NM , 24-Aug-2011) (Proof modification is discouraged.)
(New usage is discouraged.)
Ref
Expression
Hypotheses
mpteq12dv.1
⊢ ( 𝜑 → 𝐴 = 𝐶 )
mpteq12dv.2
⊢ ( 𝜑 → 𝐵 = 𝐷 )
Assertion
mpteq12dvOLD
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )
Proof
Step
Hyp
Ref
Expression
1
mpteq12dv.1
⊢ ( 𝜑 → 𝐴 = 𝐶 )
2
mpteq12dv.2
⊢ ( 𝜑 → 𝐵 = 𝐷 )
3
2
adantr
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = 𝐷 )
4
1 3
mpteq12dva
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐶 ↦ 𝐷 ) )