Theorem ssequn1 4209

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 950	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4176	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 338	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 303	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1817	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3993	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2733	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 846  ∀wal 1535   = wceq 1537   ∈ wcel 2108   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  ssequn2  4212  undif  4505  uniop  5534  pwssun  5590  cnvimassrndm  6183  unisucg  6473  ordssun  6497  ordequn  6498  onunel  6500  onun2  6503  funiunfv  7285  sorpssun  7765  ordunpr  7862  onuninsuci  7877  omun  7926  sucdom2OLD  9148  domss2  9202  findcard2s  9231  sucdom2  9269  rankopb  9921  ranksuc  9934  kmlem11  10230  fin1a2lem10  10478  trclublem  15044  trclubi  15045  trclub  15047  reltrclfv  15066  modfsummods  15841  cvgcmpce  15866  mreexexlem3d  17704  dprd2da  20086  dpjcntz  20096  dpjdisj  20097  dpjlsm  20098  dpjidcl  20102  ablfac1eu  20117  perfcls  23394  dfconn2  23448  comppfsc  23561  llycmpkgen2  23579  trfil2  23916  fixufil  23951  tsmsres  24173  ustssco  24244  ustuqtop1  24271  xrge0gsumle  24874  volsup  25610  mbfss  25700  itg2cnlem2  25817  iblss2  25861  vieta1lem2  26371  amgm  27052  wilthlem2  27130  ftalem3  27136  rpvmasum2  27574  noetalem1  27804  madeoldsuc  27941  iuninc  32583  pmtrcnel  33082  pmtrcnelor  33084  hgt750lemb  34633  rankaltopb  35943  hfun  36142  bj-prmoore  37081  nacsfix  42668  cantnfresb  43286  omabs2  43294  onsucunipr  43334  oaun2  43343  oaun3  43344  fvnonrel  43559  rclexi  43577  rtrclex  43579  trclubgNEW  43580  trclubNEW  43581  dfrtrcl5  43591  trrelsuperrel2dg  43633  iunrelexp0  43664  corcltrcl  43701  isotone1  44010  aacllem  48895