Description: Obsolete version of mpteq2da as of 11-Nov-2024. (Contributed by FL, 14-Sep-2013) (Revised by Mario Carneiro, 16-Dec-2013) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mpteq2da.1 | |- F/ x ph |
|
| mpteq2da.2 | |- ( ( ph /\ x e. A ) -> B = C ) |
||
| Assertion | mpteq2daOLD | |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mpteq2da.1 | |- F/ x ph |
|
| 2 | mpteq2da.2 | |- ( ( ph /\ x e. A ) -> B = C ) |
|
| 3 | eqid | |- A = A |
|
| 4 | 3 | ax-gen | |- A. x A = A |
| 5 | 2 | ex | |- ( ph -> ( x e. A -> B = C ) ) |
| 6 | 1 5 | ralrimi | |- ( ph -> A. x e. A B = C ) |
| 7 | mpteq12f | |- ( ( A. x A = A /\ A. x e. A B = C ) -> ( x e. A |-> B ) = ( x e. A |-> C ) ) |
|
| 8 | 4 6 7 | sylancr | |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) ) |