MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnexg Structured version   Visualization version   GIF version

Theorem rnexg 6990
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, 31-Mar-1995.)
Assertion
Ref Expression
rnexg (𝐴𝑉 → ran 𝐴 ∈ V)

Proof of Theorem rnexg
StepHypRef Expression
1 uniexg 6853 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 6853 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun2 3739 . . . 4 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5305 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3577 . . 3 ran 𝐴 𝐴
6 ssexg 4732 . . 3 ((ran 𝐴 𝐴 𝐴 ∈ V) → ran 𝐴 ∈ V)
75, 6mpan 702 . 2 ( 𝐴 ∈ V → ran 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → ran 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  Vcvv 3173  cun 3538  wss 3540   cuni 4372  dom cdm 5038  ran crn 5039
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049
This theorem is referenced by:  rnex  6992  imaexg  6995  xpexr  6999  xpexr2  7000  soex  7002  cnvexg  7005  coexg  7010  cofunexg  7023  funrnex  7026  abrexexg  7034  tposexg  7253  iunon  7323  onoviun  7327  tz7.44lem1  7388  tz7.44-3  7391  fopwdom  7953  disjen  8002  domss2  8004  domssex  8006  hartogslem2  8331  dfac12lem2  8849  unirnfdomd  9268  focdmex  13001  hashf1rnOLD  13005  hashimarn  13085  trclexlem  13581  relexp0g  13610  relexpsucnnr  13613  restval  15910  prdsbas  15940  prdsplusg  15941  prdsmulr  15942  prdsvsca  15943  prdshom  15950  sscpwex  16298  sylow1lem4  17839  sylow3lem2  17866  sylow3lem3  17867  lsmvalx  17877  txindislem  21246  xkoptsub  21267  fmfnfmlem3  21570  fmfnfmlem4  21571  ustuqtoplem  21853  ustuqtop0  21854  utopsnneiplem  21861  efabl  24100  efsubm  24101  perpln1  25405  perpln2  25406  isperp  25407  lmif  25477  islmib  25479  sizeusglecusg  26014  isgrpo  26735  grpoinvfval  26760  grpodivfval  26772  isvcOLD  26818  isnv  26851  abrexexd  28731  acunirnmpt  28841  acunirnmpt2  28842  acunirnmpt2f  28843  locfinreflem  29235  esumrnmpt2  29457  sxsigon  29582  omssubadd  29689  carsgclctunlem2  29708  pmeasadd  29714  sitgclg  29731  bnj1366  30154  ptrest  32578  elghomlem1OLD  32854  elghomlem2OLD  32855  isrngod  32867  iscringd  32967  lmhmlnmsplit  36675  rclexi  36941  rtrclexlem  36942  trclubgNEW  36944  cnvrcl0  36951  dfrtrcl5  36955  relexpmulg  37021  relexp01min  37024  relexpxpmin  37028  unirnmap  38395  unirnmapsn  38401  ssmapsn  38403  fourierdlem70  39069  fourierdlem71  39070  fourierdlem80  39079  meadjiunlem  39358  omeiunle  39407
  Copyright terms: Public domain W3C validator