![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > frn | GIF version |
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
frn | ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-f 5053 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simprbi 270 | 1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3013 ran crn 4468 Fn wfn 5044 ⟶wf 5045 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-f 5053 |
This theorem is referenced by: frnd 5205 fco2 5212 fssxp 5213 fimacnvdisj 5230 f00 5237 f0rn0 5240 f1rn 5252 f1ff1 5259 fimacnv 5467 ffvelrn 5471 f1ompt 5489 fnfvrnss 5497 rnmptss 5498 fliftrel 5609 fo1stresm 5970 fo2ndresm 5971 1stcof 5972 2ndcof 5973 fo2ndf 6030 tposf2 6071 iunon 6087 smores2 6097 map0b 6484 mapsn 6487 f1imaen2g 6590 phplem4dom 6658 isinfinf 6693 djuin 6836 updjudhcoinlf 6851 updjudhcoinrg 6852 casef 6859 unirnioo 9539 frecuzrdgdomlem 9973 frecuzrdgfunlem 9975 frecuzrdgtclt 9977 blin2 12218 tgqioo 12321 |
Copyright terms: Public domain | W3C validator |