Theorem ssequn1 3588

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 874	. . . 4 |- ( ( x e. A -> x e. B ) <-> ( x e. B <-> ( x e. A \/ x e. B ) ) )
3		elun 3559	. . . . 5 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	bibi1i 312	. . . 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 1648	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
7		dfss2 3406	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
8		dfcleq 2375	. 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 366   A.wal 1397   = wceq 1399   e. wcel 1826   u. cun 3387   C_ wss 3389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-v 3036  df-un 3394  df-in 3396  df-ss 3403

This theorem is referenced by:  ssequn2  3591  undif  3824  uniop  4664  pwssun  4700  unisuc  4868  ordssun  4891  ordequn  4892  onun2i  4907  funiunfv  6061  sorpssun  6486  ordunpr  6560  onuninsuci  6574  domss2  7595  sucdom2  7632  findcard2s  7676  rankopb  8183  ranksuc  8196  kmlem11  8453  fin1a2lem10  8702  trclublem  12833  trclubi  12834  trclub  12836  reltrclfv  12855  modfsummods  13609  cvgcmpce  13634  mreexexlem3d  15053  dprd2da  17204  dpjcntz  17214  dpjdisj  17215  dpjlsm  17216  dpjidcl  17220  dpjidclOLD  17227  ablfac1eu  17237  perfcls  19952  dfcon2  20005  comppfsc  20118  llycmpkgen2  20136  trfil2  20473  fixufil  20508  tsmsresOLD  20730  tsmsres  20731  ustssco  20802  ustuqtop1  20829  xrge0gsumle  21423  volsup  22051  mbfss  22138  itg2cnlem2  22254  iblss2  22297  vieta1lem2  22792  amgm  23437  wilthlem2  23460  ftalem3  23465  rpvmasum2  23814  iuninc  27557  rankaltopb  29782  hfun  29988  nacsfix  30810  aacllem  33550  iunrelexp0  38242  corcltrcl  38249