Theorem ssequn1 3525

Description: A relationship between subclass and union. Theorem 26 of [Suppes] p. 27. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

Ref	Expression
ssequn1	|- ( A C_ B <-> ( A u. B ) = B )

Proof of Theorem ssequn1

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 200	. . . 4 |- ( ( x e. B <-> ( x e. A \/ x e. B ) ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
2		pm4.72 871	. . . 4 |- ( ( x e. A -> x e. B ) <-> ( x e. B <-> ( x e. A \/ x e. B ) ) )
3		elun 3496	. . . . 5 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	bibi1i 314	. . . 4 |- ( ( x e. ( A u. B ) <-> x e. B ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
5	1, 2, 4	3bitr4i 277	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. ( A u. B ) <-> x e. B ) )
6	5	albii 1610	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
7		dfss2 3344	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
8		dfcleq 2436	. 2 |- ( ( A u. B ) = B <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
9	6, 7, 8	3bitr4i 277	1 |- ( A C_ B <-> ( A u. B ) = B )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   A.wal 1367   = wceq 1369   e. wcel 1756   u. cun 3325   C_ wss 3327

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-v 2973  df-un 3332  df-in 3334  df-ss 3341

This theorem is referenced by:  ssequn2  3528  undif  3758  uniop  4593  pwssun  4626  unisuc  4794  ordssun  4817  ordequn  4818  onun2i  4833  funiunfv  5964  sorpssun  6366  ordunpr  6436  onuninsuci  6450  domss2  7469  sucdom2  7506  findcard2s  7552  rankopb  8058  ranksuc  8071  kmlem11  8328  fin1a2lem10  8577  cvgcmpce  13280  mreexexlem3d  14583  dprd2da  16540  dpjcntz  16550  dpjdisj  16551  dpjlsm  16552  dpjidcl  16556  dpjidclOLD  16563  ablfac1eu  16573  perfcls  18968  dfcon2  19022  llycmpkgen2  19122  trfil2  19459  fixufil  19494  tsmsresOLD  19716  tsmsres  19717  ustssco  19788  ustuqtop1  19815  xrge0gsumle  20409  volsup  21036  mbfss  21123  itg2cnlem2  21239  iblss2  21282  vieta1lem2  21776  amgm  22383  wilthlem2  22406  ftalem3  22411  rpvmasum2  22760  iuninc  25910  rankaltopb  28009  hfun  28215  comppfsc  28577  nacsfix  29046  modfsummods  30242