Theorem rnex 7617

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 7614	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3494  ran crn 5556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  elxp4  7627  elxp5  7628  ffoss  7647  fvclex  7660  wemoiso2  7675  2ndval  7692  fo2nd  7710  ixpsnf1o  8502  bren  8518  mapen  8681  ssenen  8691  sucdom2  8714  fodomfib  8798  hartogslem1  9006  brwdom  9031  unxpwdom2  9052  noinfep  9123  r0weon  9438  fseqen  9453  acnlem  9474  infpwfien  9488  aceq3lem  9546  dfac4  9548  dfac5  9554  dfac2b  9556  dfac9  9562  dfac12lem2  9570  dfac12lem3  9571  infmap2  9640  cfflb  9681  infpssr  9730  fin23lem14  9755  fin23lem16  9757  fin23lem17  9760  fin23lem38  9771  fin23lem39  9772  axdc2lem  9870  axdc3lem2  9873  axcclem  9879  ttukeylem6  9936  wunex2  10160  wuncval2  10169  intgru  10236  wfgru  10238  qexALT  12364  seqexw  13386  hashfacen  13813  shftfval  14429  vdwapval  16309  restfn  16698  prdsval  16728  wunfunc  17169  wunnat  17226  arwval  17303  catcfuccl  17369  catcxpccl  17457  yon11  17514  yon12  17515  yon2  17516  yonpropd  17518  oppcyon  17519  yonffth  17534  yoniso  17535  plusffval  17858  grpsubfval  18147  mulgfval  18226  sylow1lem2  18724  sylow2blem1  18745  sylow2blem2  18746  sylow3lem1  18752  sylow3lem6  18757  dmdprd  19120  dprdval  19125  staffval  19618  scaffval  19652  lpival  20018  ipffval  20792  cmpsub  22008  2ndcsep  22067  1stckgen  22162  kgencn2  22165  txcmplem1  22249  blbas  23040  met1stc  23131  psmetutop  23177  nmfval  23198  dchrptlem2  25841  dchrptlem3  25842  ishpg  26545  edgval  26834  bafval  28381  vsfval  28410  foresf1o  30265  fnpreimac  30416  locfinreflem  31104  cmpcref  31114  ordtconnlem1  31167  qqhval  31215  sigapildsys  31421  dya2icoseg2  31536  dya2iocuni  31541  sxbrsigalem2  31544  sxbrsigalem5  31546  omssubadd  31558  mvtval  32747  mvrsval  32752  mstaval  32791  trpredex  33076  brrestrict  33410  relowlssretop  34647  exrecfnlem  34663  ctbssinf  34690  lindsdom  34901  indexdom  35024  heiborlem1  35104  isdrngo2  35251  isrngohom  35258  idlval  35306  isidl  35307  igenval  35354  lsatset  36141  dicval  38327  trclexi  40000  rtrclexi  40001  dfrtrcl5  40009  dfrcl2  40039  stoweidlem59  42364  fourierdlem71  42482  salgensscntex  42647  aacllem  44922