Theorem rnex 3377

Description: The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41.

Hypothesis

Ref	Expression
dmex.1	|- A e. V

Assertion

Ref	Expression
rnex	|- ran A e. V

Proof of Theorem rnex

Step	Hyp	Ref	Expression
1		dmex.1	. 2 |- A e. V
2		rnexg 3375	. 2 |- (A e. V -> ran A e. V)
3	1, 2	ax-mp 7	1 |- ran A e. V

Syntax hints:   e. wcel 962  Vcvv 1818  ran crn 3187

This theorem is referenced by:  elxp4 3469  elxp5 3470  ffoss 3727  fvclex 3872  2ndval 4098  fo2nd 4108  xpmapenlem2 4517  aceq3lem 4749  aceq5 4757  ac6lem 4771  fodom 4815  infxpidmlem8 7592  retopbas 7681  bafval 8248  0vfval 8250  vsfval 8279

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-sep 2718  ax-pow 2758  ax-pr 2795  ax-un 2882

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-v 1819  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-nul 2292  df-pw 2414  df-sn 2424  df-pr 2425  df-op 2428  df-uni 2518  df-br 2635  df-opab 2682  df-cnv 3202  df-dm 3204  df-rn 3205

Copyright terms: Public domain