Description: Deduction associated with elmapd . Reverse direction of elmapdd . (Contributed by Thierry Arnoux, 13-Oct-2025) Removed redundant hypotheses. (Revised by SN, 30-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | elmaprd.1 | |- ( ph -> F e. ( B ^m A ) ) |
|
| Assertion | elmaprd | |- ( ph -> F : A --> B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elmaprd.1 | |- ( ph -> F e. ( B ^m A ) ) |
|
| 2 | elmapi | |- ( F e. ( B ^m A ) -> F : A --> B ) |
|
| 3 | 1 2 | syl | |- ( ph -> F : A --> B ) |