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 | |- ( ph -> A = C ) |
|
mpteq12dv.2 | |- ( ph -> B = D ) |
||
Assertion | mpteq12dvOLD | |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpteq12dv.1 | |- ( ph -> A = C ) |
|
2 | mpteq12dv.2 | |- ( ph -> B = D ) |
|
3 | 2 | adantr | |- ( ( ph /\ x e. A ) -> B = D ) |
4 | 1 3 | mpteq12dva | |- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) ) |