ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  frn GIF version

Theorem frn 5376
Description: The range of a mapping. (Contributed by NM, 3-Aug-1994.)
Assertion
Ref Expression
frn (𝐹:𝐴𝐵 → ran 𝐹𝐵)

Proof of Theorem frn
StepHypRef Expression
1 df-f 5222 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 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