Description: Obsolete version of mulcncf as of 9-Apr-2025. (Contributed by Glauco Siliprandi, 29-Jun-2017) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mulcncfOLD.1 | |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) |
|
| mulcncfOLD.2 | |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) |
||
| Assertion | mulcncfOLD | |- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mulcncfOLD.1 | |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) |
|
| 2 | mulcncfOLD.2 | |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) |
|
| 3 | eqid | |- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld ) |
|
| 4 | 3 | mulcn | |- x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) |
| 5 | 4 | a1i | |- ( ph -> x. e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) ) |
| 6 | 3 5 1 2 | cncfmpt2f | |- ( ph -> ( x e. X |-> ( A x. B ) ) e. ( X -cn-> CC ) ) |