Theorem ssequn1 3669

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 872	. . . 4 |- ( ( x e. A -> x e. B ) <-> ( x e. B <-> ( x e. A \/ x e. B ) ) )
3		elun 3640	. . . . 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 1615	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
7		dfss2 3488	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
8		dfcleq 2455	. 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 1372   = wceq 1374   e. wcel 1762   u. cun 3469   C_ wss 3471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-v 3110  df-un 3476  df-in 3478  df-ss 3485

This theorem is referenced by:  ssequn2  3672  undif  3902  uniop  4745  pwssun  4781  unisuc  4949  ordssun  4972  ordequn  4973  onun2i  4988  funiunfv  6141  sorpssun  6564  ordunpr  6634  onuninsuci  6648  domss2  7668  sucdom2  7706  findcard2s  7752  rankopb  8261  ranksuc  8274  kmlem11  8531  fin1a2lem10  8780  modfsummods  13558  cvgcmpce  13583  mreexexlem3d  14892  dprd2da  16876  dpjcntz  16886  dpjdisj  16887  dpjlsm  16888  dpjidcl  16892  dpjidclOLD  16899  ablfac1eu  16909  perfcls  19627  dfcon2  19681  llycmpkgen2  19781  trfil2  20118  fixufil  20153  tsmsresOLD  20375  tsmsres  20376  ustssco  20447  ustuqtop1  20474  xrge0gsumle  21068  volsup  21696  mbfss  21783  itg2cnlem2  21899  iblss2  21942  vieta1lem2  22436  amgm  23043  wilthlem2  23066  ftalem3  23071  rpvmasum2  23420  iuninc  27089  rankaltopb  29194  hfun  29400  comppfsc  29768  nacsfix  30237  trclubg  36672