![]() |
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 5222 | . 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)) | |
2 | 1 | simprbi 275 | 1 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ⊆ wss 3131 ran crn 4629 Fn wfn 5213 ⟶wf 5214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 |
This theorem depends on definitions: df-bi 117 df-f 5222 |
This theorem is referenced by: frnd 5377 fco2 5384 fssxp 5385 fimacnvdisj 5402 f00 5409 f0rn0 5412 f1rn 5424 f1ff1 5431 fimacnv 5648 ffvelcdm 5652 f1ompt 5670 fnfvrnss 5679 rnmptss 5680 fliftrel 5796 fo1stresm 6165 fo2ndresm 6166 1stcof 6167 2ndcof 6168 fo2ndf 6231 tposf2 6272 iunon 6288 smores2 6298 map0b 6690 mapsn 6693 f1imaen2g 6796 phplem4dom 6865 isinfinf 6900 updjudhcoinlf 7082 updjudhcoinrg 7083 casef 7090 unirnioo 9976 frecuzrdgdomlem 10420 frecuzrdgfunlem 10422 frecuzrdgtclt 10424 ennnfonelemrn 12423 ctinf 12434 txuni2 13917 blin2 14093 tgqioo 14208 reeff1o 14355 |
Copyright terms: Public domain | W3C validator |