Theorem rnex 7142

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. (Contributed by NM, 7-Jul-2008.)

Hypothesis

Ref	Expression
dmex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
rnex	⊢ ran 𝐴 ∈ V

Proof of Theorem rnex

Step	Hyp	Ref	Expression
1		dmex.1	. 2 ⊢ 𝐴 ∈ V
2		rnexg 7140	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 2030  Vcvv 3231  ran crn 5144

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936  ax-un 6991

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-cnv 5151  df-dm 5153  df-rn 5154

This theorem is referenced by:  elxp4  7152  elxp5  7153  ffoss  7169  fvclex  7180  abrexexOLD  7184  wemoiso2  7196  2ndval  7213  fo2nd  7231  ixpsnf1o  7990  bren  8006  mapen  8165  ssenen  8175  sucdom2  8197  fodomfib  8281  hartogslem1  8488  brwdom  8513  unxpwdom2  8534  noinfep  8595  r0weon  8873  fseqen  8888  acnlem  8909  infpwfien  8923  aceq3lem  8981  dfac4  8983  dfac5  8989  dfac2  8991  dfac9  8996  dfac12lem2  9004  dfac12lem3  9005  infmap2  9078  cfflb  9119  infpssr  9168  fin23lem14  9193  fin23lem16  9195  fin23lem17  9198  fin23lem38  9209  fin23lem39  9210  axdc2lem  9308  axdc3lem2  9311  axcclem  9317  ttukeylem6  9374  wunex2  9598  wuncval2  9607  intgru  9674  wfgru  9676  qexALT  11841  hashfacen  13276  shftfval  13854  vdwapval  15724  restfn  16132  prdsval  16162  wunfunc  16606  wunnat  16663  arwval  16740  catcfuccl  16806  catcxpccl  16894  yon11  16951  yon12  16952  yon2  16953  yonpropd  16955  oppcyon  16956  yonffth  16971  yoniso  16972  plusffval  17294  sylow1lem2  18060  sylow2blem1  18081  sylow2blem2  18082  sylow3lem1  18088  sylow3lem6  18093  dmdprd  18443  dprdval  18448  staffval  18895  scaffval  18929  lpival  19293  ipffval  20041  cmpsub  21251  2ndcsep  21310  1stckgen  21405  kgencn2  21408  txcmplem1  21492  blbas  22282  met1stc  22373  psmetutop  22419  nmfval  22440  qtopbaslem  22609  dchrptlem2  25035  dchrptlem3  25036  ishpg  25696  edgval  25986  edgvalOLD  25987  bafval  27587  vsfval  27616  foresf1o  29469  locfinreflem  30035  cmpcref  30045  ordtconnlem1  30098  qqhval  30146  sigapildsys  30353  dya2icoseg2  30468  dya2iocuni  30473  sxbrsigalem2  30476  sxbrsigalem5  30478  omssubadd  30490  mvtval  31523  mvrsval  31528  mstaval  31567  trpredex  31861  brrestrict  32181  relowlssretop  33341  lindsdom  33533  indexdom  33659  heiborlem1  33740  isdrngo2  33887  isrngohom  33894  idlval  33942  isidl  33943  igenval  33990  lsatset  34595  dicval  36782  trclexi  38244  rtrclexi  38245  dfrtrcl5  38253  dfrcl2  38283  stoweidlem59  40594  fourierdlem71  40712  salgensscntex  40880  aacllem  42875