![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fdmd | Unicode version |
Description: Deduction form of fdm 5366. 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 5366 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-fn 5214 df-f 5215 |
This theorem is referenced by: fssdmd 5374 fssdm 5375 ctssdccl 7103 1arith 12335 ennnfonelemg 12374 ennnfonelemrnh 12387 ennnfonelemf1 12389 ctinfomlemom 12398 ctinf 12401 lmbrf 13348 cnntri 13357 cncnp 13363 lmtopcnp 13383 txcnp 13404 hmeores 13448 xmetdmdm 13489 metn0 13511 ellimc3apf 13762 limccnpcntop 13777 dvfvalap 13783 dvcjbr 13805 dvcj 13806 dvfre 13807 dvexp 13808 |
Copyright terms: Public domain | W3C validator |