Theorem ssequn1 4142

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 4110	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 341	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1852	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3925	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2759	. 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 2146   ∪ cun 3906   ⊆ wss 3908

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925

This theorem is used by:  ssequn2  4145  undif  4448  uniop  5503  pwssun  5558  cnvimassrndm  6154  unisucg  6448  ordssun  6472  ordequn  6473  onunel  6475  onun2  6478  funiunfv  7253  sorpssun  7740  ordunpr  7831  onuninsuci  7845  omun  7893  domss2  9134  findcard2s  9160  sucdom2  9197  rankopb  9834  ranksuc  9847  kmlem11  10163  fin1a2lem10  10411  trclublem  15058  trclubi  15059  trclub  15061  reltrclfv  15080  modfsummods  15871  cvgcmpce  15896  mreexexlem3d  17727  dprd2da  20145  dpjcntz  20155  dpjdisj  20156  dpjlsm  20157  dpjidcl  20161  ablfac1eu  20176  perfcls  23559  dfconn2  23613  comppfsc  23726  llycmpkgen2  23744  trfil2  24081  fixufil  24116  tsmsres  24338  ustssco  24409  ustuqtop1  24435  xrge0gsumle  25028  volsup  25752  mbfss  25842  itg2cnlem2  25958  iblss2  26002  vieta1lem2  26509  amgm  27192  wilthlem2  27270  ftalem3  27276  rpvmasum2  27713  noetalem1  27942  madeoldsuc  28115  iuninc  32942  pmtrcnel  33440  pmtrcnelor  33442  hgt750lemb  35075  rankaltopb  36492  hfun  36691  bj-prmoore  37798  nacsfix  43484  cantnfresb  44092  omabs2  44100  onsucunipr  44140  oaun2  44149  oaun3  44150  fvnonrel  44364  rclexi  44382  rtrclex  44384  trclubgNEW  44385  trclubNEW  44386  dfrtrcl5  44396  trrelsuperrel2dg  44438  iunrelexp0  44469  corcltrcl  44506  isotone1  44815  aacllem  50662