Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fndm | GIF version |
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fndm | ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 5096 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
2 | 1 | simprbi 273 | 1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 dom cdm 4509 Fun wfun 5087 Fn wfn 5088 |
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 5096 |
This theorem is referenced by: funfni 5193 fndmu 5194 fnbr 5195 fnco 5201 fnresdm 5202 fnresdisj 5203 fnssresb 5205 fn0 5212 fnimadisj 5213 fnimaeq0 5214 dmmpti 5222 fdm 5248 f1dm 5303 f1odm 5339 f1o00 5370 fvelimab 5445 fvun1 5455 eqfnfv2 5487 fndmdif 5493 fneqeql2 5497 elpreima 5507 fsn2 5562 fconst3m 5607 fconst4m 5608 fnfvima 5620 funiunfvdm 5632 fnunirn 5636 dff13 5637 f1eqcocnv 5660 oprssov 5880 offval 5957 ofrfval 5958 fnexALT 5979 dmmpo 6071 dmmpoga 6074 tposfo2 6132 smodm2 6160 smoel2 6168 tfrlem5 6179 tfrlem8 6183 tfrlem9 6184 tfrlemisucaccv 6190 tfrlemiubacc 6195 tfrexlem 6199 tfri2d 6201 tfr1onlemsucaccv 6206 tfr1onlemubacc 6211 tfrcllemsucaccv 6219 tfri2 6231 rdgivallem 6246 ixpprc 6581 ixpssmap2g 6589 ixpssmapg 6590 bren 6609 fndmeng 6672 caseinl 6944 caseinr 6945 dmaddpi 7101 dmmulpi 7102 hashinfom 10492 shftfn 10564 phimullem 11828 ennnfonelemhom 11855 qnnen 11871 cldrcl 12198 neiss2 12238 txdis1cn 12374 |
Copyright terms: Public domain | W3C validator |