Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fdmd | Unicode version |
Description: Deduction form of fdm 5337. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
fdmd.1 |
Ref | Expression |
---|---|
fdmd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdmd.1 | . 2 | |
2 | fdm 5337 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 cdm 4598 wf 5178 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-fn 5185 df-f 5186 |
This theorem is referenced by: fssdmd 5345 fssdm 5346 ctssdccl 7067 ennnfonelemg 12279 ennnfonelemrnh 12292 ennnfonelemf1 12294 ctinfomlemom 12303 ctinf 12306 lmbrf 12762 cnntri 12771 cncnp 12777 lmtopcnp 12797 txcnp 12818 hmeores 12862 xmetdmdm 12903 metn0 12925 ellimc3apf 13176 limccnpcntop 13191 dvfvalap 13197 dvcjbr 13219 dvcj 13220 dvfre 13221 dvexp 13222 |
Copyright terms: Public domain | W3C validator |