Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > frn | Unicode version |
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
frn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 5186 | . 2 | |
2 | 1 | simprbi 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wss 3111 crn 4599 wfn 5177 wf 5178 |
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-f 5186 |
This theorem is referenced by: frnd 5341 fco2 5348 fssxp 5349 fimacnvdisj 5366 f00 5373 f0rn0 5376 f1rn 5388 f1ff1 5395 fimacnv 5608 ffvelrn 5612 f1ompt 5630 fnfvrnss 5639 rnmptss 5640 fliftrel 5754 fo1stresm 6121 fo2ndresm 6122 1stcof 6123 2ndcof 6124 fo2ndf 6186 tposf2 6227 iunon 6243 smores2 6253 map0b 6644 mapsn 6647 f1imaen2g 6750 phplem4dom 6819 isinfinf 6854 updjudhcoinlf 7036 updjudhcoinrg 7037 casef 7044 unirnioo 9900 frecuzrdgdomlem 10342 frecuzrdgfunlem 10344 frecuzrdgtclt 10346 ennnfonelemrn 12295 ctinf 12306 txuni2 12803 blin2 12979 tgqioo 13094 reeff1o 13241 |
Copyright terms: Public domain | W3C validator |