Theorem uniexg 3094

Description: The ZF Axiom of Union in class notation, in the form of a theorem instead of an inference. We use the antecedent A ∈ B instead of A ∈ V to make the theorem more general and thus shorten some proofs; obviously V is one possibility for B.

Assertion

Ref	Expression
uniexg	⊢ (A ∈ B → ∪A ∈ V)

Proof of Theorem uniexg

Step	Hyp	Ref	Expression
1		unieq 2576	. . 3 ⊢ (x = A → ∪x = ∪A)
2	1	eleq1d 1583	. 2 ⊢ (x = A → (∪x ∈ V ↔ ∪A ∈ V))
3		visset 1859	. . 3 ⊢ x ∈ V
4	3	uniex 3093	. 2 ⊢ ∪x ∈ V
5	2, 4	vtoclg 1893	1 ⊢ (A ∈ B → ∪A ∈ V)

Syntax hints:   → wi 3   = wceq 992   ∈ wcel 994  Vcvv 1857  ∪cuni 2569

This theorem is referenced by:  snnex 3100  euuni 3105  uniexb 3130  ssonuni 3148  dmexg 3445  rnexg 3446  iunexg 3976  onopruni 4210  tz7.44lem1 4228  carduni 5008  cardprc 5011  suplem2pr 5316  lbinfm 6216  eltopsp 7816  istps 7818  tgval 7828  eltg 7830  eltg2 7831  cldval 7876  ntrfval 7877  clsfval 7878  iscld 7879  ntrval 7886  clsval 7887  neifval 7924  neif 7925  neiss2 7926  neival 7927  isnei 7928  lpfval 7952  lpval 7953  islp2 7957  cnpfval 7967  iscn 7968  iscnp 7970  grpinvval 8284  grpinvf 8297  spwval2 8915  pjval 9515  fiv 10849  idrval 10904  topindis 11009  homeofval 11022  idhme 11028  hmphre 11036  homcardus 11046  stoiglem 11063  qusp 11068  fillsb 11073  cnfilca 11088  sfvlim 11100  limfillem1 11101  bwt2 11123  opncldf1 11454  cncls 11473  elsubsp 11477  subspid 11478  subsubtop 11479  subcld 11480  subntr 11482  cnsubsp2 11484  compsublem 11487  compsub 11488  cptclsscpt 11489  compfipin0lem 11492  compfipin0 11493  connsub 11502  isfne 11541  isref 11549  locfindsc 11576  topjoin 11588  fnejoin1 11591  fgf 11632  elfg 11633  ufilss 11652  ufileu 11658  filufint 11659  uffixfr 11660  filcon 11665  limfil 11675  flimcls 11684  cnpfillim 11686  filmapf 11688  isfilmap 11689  elfilmap3 11692  fmfnfmlem4 11703  fmfnfm 11704  flimff 11707  sflimf 11708  isflimf 11709  flimfnei 11710  flimfcnp 11714  sfcls 11716  fcluscf 11724  flimfnfcls 11727  fcluscnplem 11729  fcluscnp 11730  fcluscomp 11733  fclusff 11735  sfclusf 11736  isfclusf 11737  flfssfcf 11741  uffcfflf 11742  tailf 11756  istail 11757  tailmap 11759  filnetlem4 11766  filnet 11768  supex2g 11853  subspopn 11900  subspabs 11903  cnimass 11949  cnres 11950  cnresima 11952  cnss 11953  ishomeo2 11957  tlmval 11964  txuni 11975  tx1cn 11976  tx2cn 11977  uptx 11978  txcn 11979  txsubsp 11983

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-uni 2570

Copyright terms: Public domain