Theorem ssequn1 4149

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 222	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 951	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4116	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 338	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 303	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3931	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2722	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ∪ cun 3912   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  ssequn2  4152  undif  4445  uniop  5475  pwssun  5530  cnvimassrndm  6125  unisucg  6412  ordssun  6436  ordequn  6437  onunel  6439  onun2  6442  funiunfv  7222  sorpssun  7706  ordunpr  7801  onuninsuci  7816  omun  7864  domss2  9100  findcard2s  9129  sucdom2  9167  rankopb  9805  ranksuc  9818  kmlem11  10114  fin1a2lem10  10362  trclublem  14961  trclubi  14962  trclub  14964  reltrclfv  14983  modfsummods  15759  cvgcmpce  15784  mreexexlem3d  17607  dprd2da  19974  dpjcntz  19984  dpjdisj  19985  dpjlsm  19986  dpjidcl  19990  ablfac1eu  20005  perfcls  23252  dfconn2  23306  comppfsc  23419  llycmpkgen2  23437  trfil2  23774  fixufil  23809  tsmsres  24031  ustssco  24102  ustuqtop1  24129  xrge0gsumle  24722  volsup  25457  mbfss  25547  itg2cnlem2  25663  iblss2  25707  vieta1lem2  26219  amgm  26901  wilthlem2  26979  ftalem3  26985  rpvmasum2  27423  noetalem1  27653  madeoldsuc  27796  iuninc  32489  pmtrcnel  33046  pmtrcnelor  33048  hgt750lemb  34647  rankaltopb  35967  hfun  36166  bj-prmoore  37103  nacsfix  42700  cantnfresb  43313  omabs2  43321  onsucunipr  43361  oaun2  43370  oaun3  43371  fvnonrel  43586  rclexi  43604  rtrclex  43606  trclubgNEW  43607  trclubNEW  43608  dfrtrcl5  43618  trrelsuperrel2dg  43660  iunrelexp0  43691  corcltrcl  43728  isotone1  44037  aacllem  49787