Theorem uniss 4270

Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39. (Contributed by NM, 22-Mar-1998.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Assertion

Ref	Expression
uniss

Proof of Theorem uniss

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3497	. . . . 5
2	1	anim2d 565	. . . 4
3	2	eximdv 1710	. . 3
4		eluni 4252	. . 3
5		eluni 4252	. . 3
6	3, 4, 5	3imtr4g 270	. 2
7	6	ssrdv 3509	1

Syntax hints:  ->wi 4  /\wa 369  E.wex 1612  e.wcel 1818  C_wss 3475  U.cuni 4249

This theorem is referenced by:  unissi  4272  unissd  4273  intssuni2  4312  uniintsn  4324  relfld  5538  dffv2  5946  trcl  8180  cflm  8651  coflim  8662  cfslbn  8668  fin23lem41  8753  fin1a2lem12  8812  tskuni  9182  prdsval  14852  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdshom  14864  mrcssv  15011  catcfuccl  15436  catcxpccl  15476  mrelatlub  15816  mreclatBAD  15817  dprdres  17075  dmdprdsplit2lem  17094  tgcl  19471  distop  19497  fctop  19505  cctop  19507  neiptoptop  19632  cmpcld  19902  uncmp  19903  cmpfi  19908  bwthOLD  19911  comppfsc  20033  kgentopon  20039  txcmplem2  20143  filcon  20384  alexsubALTlem3  20549  alexsubALT  20551  ptcmplem3  20554  dyadmbllem  22008  shsupcl  26256  hsupss  26259  shatomistici  27280  cvmliftlem15  28743  frrlem5c  29393  filnetlem3  30198  heiborlem1  30307  lssats  34737  lpssat  34738  lssatle  34740  lssat  34741  dicval  36903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250