Theorem ssequn1 4184

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861  ∀wal 1567   = wceq 1569   ∈ wcel 2144   ⊆ wss 3895   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-un 4151

This theorem is used by:  ssequn2  4187  undif  4437  uniop  5487  pwssun  5542  cnvimassrndmOLD  6199  unisucg  6443  ordssun  6467  ordequn  6468  onunel  6470  onun2  6473  funiunfv  7252  sorpssun  7746  ordunpr  7837  onuninsuci  7851  omun  7899  domss2  9158  findcard2s  9184  sucdom2  9221  rankopb  9869  ranksuc  9885  hfunOLD  9922  kmlem11  10242  fin1a2lem10  10490  trclublem  15153  trclubi  15154  trclub  15156  reltrclfv  15175  modfsummods  15965  cvgcmpce  15990  mreexexlem3d  17825  dprd2da  20263  dpjcntz  20273  dpjdisj  20274  dpjlsm  20275  dpjidcl  20279  ablfac1eu  20294  perfcls  23688  dfconn2  23742  comppfsc  23856  llycmpkgen2  23874  trfil2  24211  fixufil  24246  tsmsres  24468  ustssco  24539  ustuqtop1  24565  xrge0gsumle  25158  volsup  25882  mbfss  25972  itg2cnlem2  26088  iblss2  26131  vieta1lem2  26639  amgm  27323  wilthlem2  27401  ftalem3  27407  rpvmasum2  27844  noetalem1  28103  madeoldsuc  28276  iuninc  33202  pmtrcnel  33696  pmtrcnelor  33698  hgt750lemb  35331  ordunmax  35765  rankaltopb  36836  bj-prmoore  38128  nacsfix  43816  cantnfresb  44419  omabs2  44427  onsucunipr  44467  oaun2  44476  oaun3  44477  fvnonrel  44690  rclexi  44708  rtrclex  44710  trclubgNEW  44711  trclubNEW  44712  dfrtrcl5  44722  trrelsuperrel2dg  44764  iunrelexp0  44795  corcltrcl  44832  isotone1  45141  tmachlem-agreeprod  48040  aacllem  51107