Theorem uniss 2516

Description: Subclass relationship for class union. Theorem 61 of [Suppes] p. 39.

Assertion

Ref	Expression
uniss	|- (A (_ B -> U.A (_ U.B)

Proof of Theorem uniss

Step	Hyp	Ref	Expression
1		ssel 2059	. . . . . 6 |- (A (_ B -> (y e. A -> y e. B))
2	1	anim2d 560	. . . . 5 |- (A (_ B -> ((x e. y /\ y e. A) -> (x e. y /\ y e. B)))
3	2	19.22dv 1288	. . . 4 |- (A (_ B -> (E.y(x e. y /\ y e. A) -> E.y(x e. y /\ y e. B)))
4	3	19.21aiv 1284	. . 3 |- (A (_ B -> A.x(E.y(x e. y /\ y e. A) -> E.y(x e. y /\ y e. B)))
5		ss2ab 2112	. . 3 |- ({x | E.y(x e. y /\ y e. A)} (_ {x | E.y(x e. y /\ y e. B)} <-> A.x(E.y(x e. y /\ y e. A) -> E.y(x e. y /\ y e. B)))
6	4, 5	sylibr 200	. 2 |- (A (_ B -> {x | E.y(x e. y /\ y e. A)} (_ {x | E.y(x e. y /\ y e. B)})
7		df-uni 2499	. 2 |- U.A = {x | E.y(x e. y /\ y e. A)}
8		df-uni 2499	. 2 |- U.B = {x | E.y(x e. y /\ y e. B)}
9	6, 7, 8	3sstr4g 2098	1 |- (A (_ B -> U.A (_ U.B)

Syntax hints:   -> wi 3   /\ wa 223  A.wal 952   e. wcel 956  E.wex 978  {cab 1461   (_ wss 2043  U.cuni 2498

This theorem is referenced by:  unidif 2525  intssuni2 2551  sspwuni 2753  unixpss 3253  relfld 3507  unixp0 3510  trcl 4625  rankuni 4678  cflim 4889  unirnioo 6343  tgval2t 7567  unitgt 7573  tgclt 7574  tgsst 7586  basgen2t 7589  subbas2 7595  distop 7599  fctop 7600  cctop 7602  cncnplem1 7724  uniopn 7813  opnuni 7820  unirnbl 7827  dfchsup2 9236  hsupval2t 9238  hsupvalt 9239  shsupclt 9244  hsupss 9247  shsupunss 9253  shatomistic 10225  fgsb 10480

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-uni 2499

Copyright terms: Public domain