Theorem ssequn1 3636

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 203	. . . 4 |- ( ( x e. B <-> ( x e. A \/ x e. B ) ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
2		pm4.72 884	. . . 4 |- ( ( x e. A -> x e. B ) <-> ( x e. B <-> ( x e. A \/ x e. B ) ) )
3		elun 3606	. . . . 5 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	bibi1i 315	. . . 4 |- ( ( x e. ( A u. B ) <-> x e. B ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
5	1, 2, 4	3bitr4i 280	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. ( A u. B ) <-> x e. B ) )
6	5	albii 1687	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
7		dfss2 3453	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
8		dfcleq 2415	. 2 |- ( ( A u. B ) = B <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
9	6, 7, 8	3bitr4i 280	1 |- ( A C_ B <-> ( A u. B ) = B )

Syntax hints:   -> wi 4   <-> wb 187   \/ wo 369   A.wal 1435   = wceq 1437   e. wcel 1868   u. cun 3434   C_ wss 3436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-v 3083  df-un 3441  df-in 3443  df-ss 3450

This theorem is referenced by:  ssequn2  3639  undif  3876  uniop  4719  pwssun  4755  unisuc  5514  ordssun  5537  ordequn  5538  onun2i  5553  funiunfv  6164  sorpssun  6588  ordunpr  6663  onuninsuci  6677  domss2  7733  sucdom2  7770  findcard2s  7814  rankopb  8324  ranksuc  8337  kmlem11  8590  fin1a2lem10  8839  trclublem  13047  trclubi  13048  trclub  13050  reltrclfv  13069  modfsummods  13840  cvgcmpce  13865  mreexexlem3d  15539  dprd2da  17662  dpjcntz  17672  dpjdisj  17673  dpjlsm  17674  dpjidcl  17678  ablfac1eu  17693  perfcls  20367  dfcon2  20420  comppfsc  20533  llycmpkgen2  20551  trfil2  20888  fixufil  20923  tsmsres  21144  ustssco  21215  ustuqtop1  21242  xrge0gsumle  21837  volsup  22495  mbfss  22588  itg2cnlem2  22706  iblss2  22749  vieta1lem2  23250  amgm  23902  wilthlem2  23980  ftalem3  23985  rpvmasum2  24336  iuninc  28165  rankaltopb  30738  hfun  30937  nacsfix  35472  trrelsuperrel2dg  36122  iunrelexp0  36153  corcltrcl  36190  aacllem  39813