Theorem dmexg 3354

Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26.

Assertion

Ref	Expression
dmexg	|- (A e. B -> dom A e. V)

Proof of Theorem dmexg

Step	Hyp	Ref	Expression
1		uniexg 2867	. 2 |- (A e. B -> U.A e. V)
2		uniexg 2867	. 2 |- (U.A e. V -> U.U.A e. V)
3		ssun1 2190	. . . 4 |- dom A (_ (dom A u. ran A)
4		dmrnssfld 3353	. . . 4 |- (dom A u. ran A) (_ U.U.A
5	3, 4	sstri 2070	. . 3 |- dom A (_ U.U.A
6		ssexg 2717	. . 3 |- ((dom A (_ U.U.A /\ U.U.A e. V) -> dom A e. V)
7	5, 6	mpan 694	. 2 |- (U.U.A e. V -> dom A e. V)
8	1, 2, 7	3syl 20	1 |- (A e. B -> dom A e. V)

Syntax hints:   -> wi 3   e. wcel 957  Vcvv 1808   u. cun 2042   (_ wss 2044  U.cuni 2499  dom cdm 3166  ran crn 3167

This theorem is referenced by:  dmex 3356  inelv 3358  xpexr2 3476  cnvexg 3515  coexg 3520  cofunexg 3576  dmfex 3650  imadomg 4789  ismet 7758  metxp 7796  blfval 7797  blval 7799  blrn 7803  blf 7806  opnfval 7819  isopn 7821  lmfval 7887  caufval 7888  lmbr 7890  iscau 7898  bcthlem12 7972  bcthlem15 7975  bcthlem30 7990

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-10 965  ax-11 966  ax-12 967  ax-13 968  ax-14 969  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217  ax-ext 1458  ax-sep 2699  ax-pow 2738  ax-pr 2775  ax-un 2862

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 980  df-sb 1171  df-eu 1381  df-mo 1382  df-clab 1463  df-cleq 1468  df-clel 1471  df-ne 1585  df-v 1809  df-dif 2046  df-un 2047  df-in 2048  df-ss 2050  df-nul 2278  df-pw 2399  df-sn 2409  df-pr 2410  df-op 2413  df-uni 2500  df-br 2616  df-opab 2663  df-cnv 3182  df-dm 3184  df-rn 3185

Copyright terms: Public domain