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

Theorem frn 5281
 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 5127 . 2 (𝐹:𝐴𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹𝐵))
21simprbi 273 1 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
 Colors of variables: wff set class Syntax hints:   → wi 4   ⊆ wss 3071  ran crn 4540   Fn wfn 5118  ⟶wf 5119 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 5127 This theorem is referenced by:  frnd  5282  fco2  5289  fssxp  5290  fimacnvdisj  5307  f00  5314  f0rn0  5317  f1rn  5329  f1ff1  5336  fimacnv  5549  ffvelrn  5553  f1ompt  5571  fnfvrnss  5580  rnmptss  5581  fliftrel  5693  fo1stresm  6059  fo2ndresm  6060  1stcof  6061  2ndcof  6062  fo2ndf  6124  tposf2  6165  iunon  6181  smores2  6191  map0b  6581  mapsn  6584  f1imaen2g  6687  phplem4dom  6756  isinfinf  6791  updjudhcoinlf  6965  updjudhcoinrg  6966  casef  6973  unirnioo  9768  frecuzrdgdomlem  10202  frecuzrdgfunlem  10204  frecuzrdgtclt  10206  ennnfonelemrn  11943  ctinf  11954  txuni2  12439  blin2  12615  tgqioo  12730  reeff1o  12877
 Copyright terms: Public domain W3C validator