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 ) ) |