Theorem ssequn1 4135

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 964	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4103	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 341	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3919	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2755	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ∪ cun 3900   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  ssequn2  4138  undif  4441  uniop  5496  pwssun  5551  cnvimassrndm  6147  unisucg  6442  ordssun  6466  ordequn  6467  onunel  6469  onun2  6472  funiunfv  7248  sorpssun  7734  ordunpr  7825  onuninsuci  7839  omun  7887  domss2  9137  findcard2s  9163  sucdom2  9200  rankopb  9837  ranksuc  9850  kmlem11  10166  fin1a2lem10  10414  trclublem  15070  trclubi  15071  trclub  15073  reltrclfv  15092  modfsummods  15882  cvgcmpce  15907  mreexexlem3d  17738  dprd2da  20172  dpjcntz  20182  dpjdisj  20183  dpjlsm  20184  dpjidcl  20188  ablfac1eu  20203  perfcls  23591  dfconn2  23645  comppfsc  23759  llycmpkgen2  23777  trfil2  24114  fixufil  24149  tsmsres  24371  ustssco  24442  ustuqtop1  24468  xrge0gsumle  25061  volsup  25785  mbfss  25875  itg2cnlem2  25991  iblss2  26035  vieta1lem2  26542  amgm  27225  wilthlem2  27303  ftalem3  27309  rpvmasum2  27746  noetalem1  27975  madeoldsuc  28148  iuninc  33020  pmtrcnel  33516  pmtrcnelor  33518  hgt750lemb  35151  rankaltopb  36546  hfun  36745  bj-prmoore  37852  nacsfix  43544  cantnfresb  44152  omabs2  44160  onsucunipr  44200  oaun2  44209  oaun3  44210  fvnonrel  44424  rclexi  44442  rtrclex  44444  trclubgNEW  44445  trclubNEW  44446  dfrtrcl5  44456  trrelsuperrel2dg  44498  iunrelexp0  44529  corcltrcl  44566  isotone1  44875  tmachlem-agreeprod  47752  aacllem  50759