Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fdmd | GIF version |
Description: Deduction form of fdm 5351. 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 5351 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1348 dom cdm 4609 ⟶wf 5192 |
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 5199 df-f 5200 |
This theorem is referenced by: fssdmd 5359 fssdm 5360 ctssdccl 7084 1arith 12306 ennnfonelemg 12345 ennnfonelemrnh 12358 ennnfonelemf1 12360 ctinfomlemom 12369 ctinf 12372 lmbrf 12968 cnntri 12977 cncnp 12983 lmtopcnp 13003 txcnp 13024 hmeores 13068 xmetdmdm 13109 metn0 13131 ellimc3apf 13382 limccnpcntop 13397 dvfvalap 13403 dvcjbr 13425 dvcj 13426 dvfre 13427 dvexp 13428 |
Copyright terms: Public domain | W3C validator |