Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fdmd | Unicode version |
Description: Deduction form of fdm 5278. 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 5278 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cdm 4539 wf 5119 |
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 5126 df-f 5127 |
This theorem is referenced by: fssdmd 5286 fssdm 5287 ctssdccl 6996 ennnfonelemg 11921 ennnfonelemrnh 11934 ennnfonelemf1 11936 ctinfomlemom 11945 ctinf 11948 lmbrf 12389 cnntri 12398 cncnp 12404 lmtopcnp 12424 txcnp 12445 hmeores 12489 xmetdmdm 12530 metn0 12552 ellimc3apf 12803 limccnpcntop 12818 dvfvalap 12824 dvcjbr 12846 dvcj 12847 dvfre 12848 dvexp 12849 |
Copyright terms: Public domain | W3C validator |