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
⊢ φ → A = C
mpteq12dv.2
⊢ φ → B = D
Assertion
mpteq12dvOLD
⊢ φ → x ∈ A ⟼ B = x ∈ C ⟼ D
Proof
Step
Hyp
Ref
Expression
1
mpteq12dv.1
⊢ φ → A = C
2
mpteq12dv.2
⊢ φ → B = D
3
2
adantr
⊢ φ ∧ x ∈ A → B = D
4
1 3
mpteq12dva
⊢ φ → x ∈ A ⟼ B = x ∈ C ⟼ D