Theorem ssequn1 4107

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	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Proof of Theorem ssequn1

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bicom 225	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 947	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4076	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 342	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3901	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2792	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844  ∀wal 1536   = wceq 1538   ∈ wcel 2111   ∪ cun 3879   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898

This theorem is referenced by:  ssequn2  4110  undif  4388  uniop  5370  pwssun  5421  unisuc  6235  ordssun  6258  ordequn  6259  onun2i  6274  funiunfv  6985  sorpssun  7436  ordunpr  7521  onuninsuci  7535  sucdom2  8610  domss2  8660  findcard2s  8743  rankopb  9265  ranksuc  9278  kmlem11  9571  fin1a2lem10  9820  trclublem  14346  trclubi  14347  trclub  14349  reltrclfv  14368  modfsummods  15140  cvgcmpce  15165  mreexexlem3d  16909  dprd2da  19157  dpjcntz  19167  dpjdisj  19168  dpjlsm  19169  dpjidcl  19173  ablfac1eu  19188  perfcls  21970  dfconn2  22024  comppfsc  22137  llycmpkgen2  22155  trfil2  22492  fixufil  22527  tsmsres  22749  ustssco  22820  ustuqtop1  22847  xrge0gsumle  23438  volsup  24160  mbfss  24250  itg2cnlem2  24366  iblss2  24409  vieta1lem2  24907  amgm  25576  wilthlem2  25654  ftalem3  25660  rpvmasum2  26096  iuninc  30324  pmtrcnel  30783  pmtrcnelor  30785  hgt750lemb  32037  rankaltopb  33553  hfun  33752  bj-prmoore  34530  nacsfix  39653  fvnonrel  40297  rclexi  40315  rtrclex  40317  trclubgNEW  40318  trclubNEW  40319  dfrtrcl5  40329  trrelsuperrel2dg  40372  iunrelexp0  40403  corcltrcl  40440  isotone1  40751  aacllem  45329