Theorem ssequn1 3616

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 205	. . . 4 |- ( ( x e. B <-> ( x e. A \/ x e. B ) ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
2		pm4.72 892	. . . 4 |- ( ( x e. A -> x e. B ) <-> ( x e. B <-> ( x e. A \/ x e. B ) ) )
3		elun 3586	. . . . 5 |- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
4	3	bibi1i 320	. . . 4 |- ( ( x e. ( A u. B ) <-> x e. B ) <-> ( ( x e. A \/ x e. B ) <-> x e. B ) )
5	1, 2, 4	3bitr4i 285	. . 3 |- ( ( x e. A -> x e. B ) <-> ( x e. ( A u. B ) <-> x e. B ) )
6	5	albii 1702	. 2 |- ( A. x ( x e. A -> x e. B ) <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
7		dfss2 3433	. 2 |- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
8		dfcleq 2456	. 2 |- ( ( A u. B ) = B <-> A. x ( x e. ( A u. B ) <-> x e. B ) )
9	6, 7, 8	3bitr4i 285	1 |- ( A C_ B <-> ( A u. B ) = B )

Syntax hints:   -> wi 4   <-> wb 189   \/ wo 374   A.wal 1453   = wceq 1455   e. wcel 1898   u. cun 3414   C_ wss 3416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430

This theorem is referenced by:  ssequn2  3619  undif  3860  uniop  4721  pwssun  4762  unisuc  5522  ordssun  5545  ordequn  5546  onun2i  5561  funiunfv  6183  sorpssun  6610  ordunpr  6685  onuninsuci  6699  domss2  7762  sucdom2  7799  findcard2s  7843  rankopb  8354  ranksuc  8367  kmlem11  8621  fin1a2lem10  8870  trclublem  13114  trclubi  13115  trclub  13117  reltrclfv  13136  modfsummods  13908  cvgcmpce  13933  mreexexlem3d  15607  dprd2da  17730  dpjcntz  17740  dpjdisj  17741  dpjlsm  17742  dpjidcl  17746  ablfac1eu  17761  perfcls  20436  dfcon2  20489  comppfsc  20602  llycmpkgen2  20620  trfil2  20957  fixufil  20992  tsmsres  21213  ustssco  21284  ustuqtop1  21311  xrge0gsumle  21906  volsup  22565  mbfss  22658  itg2cnlem2  22776  iblss2  22819  vieta1lem2  23320  amgm  23972  wilthlem2  24050  ftalem3  24055  rpvmasum2  24406  iuninc  28230  rankaltopb  30796  hfun  30995  nacsfix  35600  fvnonrel  36249  rclexi  36268  rtrclex  36270  trclubgNEW  36271  trclubNEW  36272  dfrtrcl5  36282  trrelsuperrel2dg  36309  iunrelexp0  36340  corcltrcl  36377  aacllem  40909