Theorem rnexg 3359

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 2871	. 2 |- (A e. B -> U.A e. V)
2		uniexg 2871	. 2 |- (U.A e. V -> U.U.A e. V)
3		ssun2 2194	. . . 4 |- ran A (_ (dom A u. ran A)
4		dmrnssfld 3357	. . . 4 |- (dom A u. ran A) (_ U.U.A
5	3, 4	sstri 2073	. . 3 |- ran A (_ U.U.A
6		ssexg 2721	. . 3 |- ((ran A (_ U.U.A /\ U.U.A e. V) -> ran A e. V)
7	5, 6	mpan 695	. 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 958  Vcvv 1811   u. cun 2045   (_ wss 2047  U.cuni 2503  dom cdm 3170  ran crn 3171

This theorem is referenced by:  rnex 3361  imaexg 3416  xpexr 3479  xpexr2 3480  cnvexg 3519  coexg 3524  cofunexg 3580  funrnex 3613  tz7.44lem1 3927  qsexg 4294  isgrp 8041  grpidval 8058  grpinvfval 8066  grpinvval 8067  grpinvf 8079  grpdivfval 8081  grplactfval 8096  issubgi 8122  ghgrpilem4 8136  isvc 8200  isnv 8231  elghomlem1 10382  elghomlem2 10383  cayleylem1 10409  cayleylem2 10410  cayleylem3 10411  cayleythlem 10413  rcfpfil 10597  rcfpfilOLD 10598  aidm 10683  aidmold 10684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-cnv 3186  df-dm 3188  df-rn 3189

Copyright terms: Public domain