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 5122 | . 2 | |
2 | 1 | simprbi 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wss 3066 crn 4535 wfn 5113 wf 5114 |
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 5122 |
This theorem is referenced by: frnd 5277 fco2 5284 fssxp 5285 fimacnvdisj 5302 f00 5309 f0rn0 5312 f1rn 5324 f1ff1 5331 fimacnv 5542 ffvelrn 5546 f1ompt 5564 fnfvrnss 5573 rnmptss 5574 fliftrel 5686 fo1stresm 6052 fo2ndresm 6053 1stcof 6054 2ndcof 6055 fo2ndf 6117 tposf2 6158 iunon 6174 smores2 6184 map0b 6574 mapsn 6577 f1imaen2g 6680 phplem4dom 6749 isinfinf 6784 updjudhcoinlf 6958 updjudhcoinrg 6959 casef 6966 unirnioo 9749 frecuzrdgdomlem 10183 frecuzrdgfunlem 10185 frecuzrdgtclt 10187 ennnfonelemrn 11921 ctinf 11932 txuni2 12414 blin2 12590 tgqioo 12705 |
Copyright terms: Public domain | W3C validator |