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

Theorem rnexg 7052
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 6915 . 2 (𝐴𝑉 𝐴 ∈ V)
2 uniexg 6915 . 2 ( 𝐴 ∈ V → 𝐴 ∈ V)
3 ssun2 3760 . . . 4 ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4 dmrnssfld 5349 . . . 4 (dom 𝐴 ∪ ran 𝐴) ⊆ 𝐴
53, 4sstri 3596 . . 3 ran 𝐴 𝐴
6 ssexg 4769 . . 3 ((ran 𝐴 𝐴 𝐴 ∈ V) → ran 𝐴 ∈ V)
75, 6mpan 705 . 2 ( 𝐴 ∈ V → ran 𝐴 ∈ V)
81, 2, 73syl 18 1 (𝐴𝑉 → ran 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  Vcvv 3189  cun 3557  wss 3559   cuni 4407  dom cdm 5079  ran crn 5080
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-rab 2916  df-v 3191  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-cnv 5087  df-dm 5089  df-rn 5090
This theorem is referenced by:  rnex  7054  imaexg  7057  xpexr  7060  xpexr2  7061  soex  7063  cnvexg  7066  coexg  7071  cofunexg  7084  funrnex  7087  abrexexg  7095  tposexg  7318  iunon  7388  onoviun  7392  tz7.44lem1  7453  tz7.44-3  7456  fopwdom  8019  disjen  8068  domss2  8070  domssex  8072  hartogslem2  8399  dfac12lem2  8917  unirnfdomd  9340  focdmex  13086  hashf1rnOLD  13090  hashimarn  13172  trclexlem  13674  relexp0g  13703  relexpsucnnr  13706  restval  16015  prdsbas  16045  prdsplusg  16046  prdsmulr  16047  prdsvsca  16048  prdshom  16055  sscpwex  16403  sylow1lem4  17944  sylow3lem2  17971  sylow3lem3  17972  lsmvalx  17982  txindislem  21355  xkoptsub  21376  fmfnfmlem3  21679  fmfnfmlem4  21680  ustuqtoplem  21962  ustuqtop0  21963  utopsnneiplem  21970  efabl  24213  efsubm  24214  perpln1  25518  perpln2  25519  isperp  25520  lmif  25590  islmib  25592  isgrpo  27218  grpoinvfval  27243  grpodivfval  27255  isvcOLD  27301  isnv  27334  abrexexd  29212  acunirnmpt  29319  acunirnmpt2  29320  acunirnmpt2f  29321  locfinreflem  29707  esumrnmpt2  29929  sxsigon  30054  omssubadd  30161  carsgclctunlem2  30180  pmeasadd  30186  sitgclg  30203  bnj1366  30635  ptrest  33067  elghomlem1OLD  33343  elghomlem2OLD  33344  isrngod  33356  iscringd  33456  lmhmlnmsplit  37164  rclexi  37430  rtrclexlem  37431  trclubgNEW  37433  cnvrcl0  37440  dfrtrcl5  37444  relexpmulg  37510  relexp01min  37513  relexpxpmin  37517  unirnmap  38897  unirnmapsn  38903  ssmapsn  38905  fourierdlem70  39721  fourierdlem71  39722  fourierdlem80  39731  meadjiunlem  40010  omeiunle  40059
  Copyright terms: Public domain W3C validator