![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fdmd | GIF version |
Description: Deduction form of fdm 5393. The domain of a mapping. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
Ref | Expression |
---|---|
fdmd.1 | ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
Ref | Expression |
---|---|
fdmd | ⊢ (𝜑 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fdmd.1 | . 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) | |
2 | fdm 5393 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1364 dom cdm 4647 ⟶wf 5234 |
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 5241 df-f 5242 |
This theorem is referenced by: fssdmd 5401 fssdm 5402 ctssdccl 7144 1arith 12410 ennnfonelemg 12465 ennnfonelemrnh 12478 ennnfonelemf1 12480 ctinfomlemom 12489 ctinf 12492 igsumval 12877 ghmrn 13221 psrbaglesuppg 13975 lmbrf 14200 cnntri 14209 cncnp 14215 lmtopcnp 14235 txcnp 14256 hmeores 14300 xmetdmdm 14341 metn0 14363 ellimc3apf 14614 limccnpcntop 14629 dvfvalap 14635 dvcjbr 14657 dvcj 14658 dvfre 14659 dvexp 14660 |
Copyright terms: Public domain | W3C validator |