Theorem rnexg 3345

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.

Assertion

Ref	Expression
rnexg	|- (A e. B -> ran A e. V)

Proof of Theorem rnexg

Step	Hyp	Ref	Expression
1		uniexg 2862	. 2 |- (A e. B -> U.A e. V)
2		uniexg 2862	. 2 |- (U.A e. V -> U.U.A e. V)
3		ssun2 2184	. . . 4 |- ran A (_ (dom A u. ran A)
4		dmrnssfld 3343	. . . 4 |- (dom A u. ran A) (_ U.U.A
5	3, 4	sstri 2063	. . 3 |- ran A (_ U.U.A
6		ssexg 2711	. . 3 |- ((ran A (_ U.U.A /\ U.U.A e. V) -> ran A e. V)
7	5, 6	mpan 693	. 2 |- (U.U.A e. V -> ran A e. V)
8	1, 2, 7	3syl 20	1 |- (A e. B -> ran A e. V)

Syntax hints:   -> wi 3   e. wcel 955  Vcvv 1802   u. cun 2035   (_ wss 2037  U.cuni 2493  dom cdm 3160  ran crn 3161

This theorem is referenced by:  imaexg 3400  elxp4 3439  elxp5 3440  xpexr 3465  xpexr2 3466  cnvexg 3505  coexg 3510  cofunexg 3566  funrnex 3599  ffoss 3696  fvclex 3841  tz7.44lem1 3912  2ndval 4066  fo2nd 4076  qsexg 4278  xpmapenlem2 4477  aceq3lem 4704  aceq5 4712  ac6lem 4726  fodom 4770  infxpidmlem8 7502  retopbas 7597  isgrp 7975  grpidval 7992  grpinvfval 8000  grpinvval 8001  grpinvf 8014  grpdivfval 8016  grplactfval 8032  issubgi 8059  ghgrpilem4 8073  isvc 8138  bafval 8161  0vfval 8163  isnv 8170  vsfval 8194  elghomlem1 10287  elghomlem2 10288  cayleylem1 10316  cayleylem2 10317  cayleylem3 10318  cayleythlem 10320  aidm 10527  aidmold 10528

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-11 964  ax-12 965  ax-13 966  ax-14 967  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452  ax-sep 2693  ax-pow 2732  ax-pr 2769  ax-un 2857

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-eu 1375  df-mo 1376  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-v 1803  df-dif 2039  df-un 2040  df-in 2041  df-ss 2043  df-nul 2271  df-pw 2392  df-sn 2402  df-pr 2403  df-op 2406  df-uni 2494  df-br 2610  df-opab 2657  df-cnv 3176  df-dm 3178  df-rn 3179

Copyright terms: Public domain