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  7249  sorpssun  7735  ordunpr  7826  onuninsuci  7840  omun  7888  domss2  9138  findcard2s  9164  sucdom2  9201  rankopb  9838  ranksuc  9851  kmlem11  10167  fin1a2lem10  10415  trclublem  15072  trclubi  15073  trclub  15075  reltrclfv  15094  modfsummods  15884  cvgcmpce  15909  mreexexlem3d  17740  dprd2da  20177  dpjcntz  20187  dpjdisj  20188  dpjlsm  20189  dpjidcl  20193  ablfac1eu  20208  perfcls  23596  dfconn2  23650  comppfsc  23764  llycmpkgen2  23782  trfil2  24119  fixufil  24154  tsmsres  24376  ustssco  24447  ustuqtop1  24473  xrge0gsumle  25066  volsup  25790  mbfss  25880  itg2cnlem2  25996  iblss2  26040  vieta1lem2  26550  amgm  27235  wilthlem2  27313  ftalem3  27319  rpvmasum2  27756  noetalem1  27985  madeoldsuc  28158  iuninc  33042  pmtrcnel  33537  pmtrcnelor  33539  hgt750lemb  35172  rankaltopb  36567  hfun  36766  bj-prmoore  37873  nacsfix  43565  cantnfresb  44173  omabs2  44181  onsucunipr  44221  oaun2  44230  oaun3  44231  fvnonrel  44445  rclexi  44463  rtrclex  44465  trclubgNEW  44466  trclubNEW  44467  dfrtrcl5  44477  trrelsuperrel2dg  44519  iunrelexp0  44550  corcltrcl  44587  isotone1  44896  tmachlem-agreeprod  47773  aacllem  50780