Theorem ssequn1 4136

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1539   = wceq 1541   ∈ wcel 2111   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  ssequn2  4139  undif  4432  uniop  5455  pwssun  5508  cnvimassrndm  6099  unisucg  6386  ordssun  6410  ordequn  6411  onunel  6413  onun2  6416  funiunfv  7182  sorpssun  7663  ordunpr  7756  onuninsuci  7770  omun  7818  domss2  9049  findcard2s  9075  sucdom2  9112  rankopb  9745  ranksuc  9758  kmlem11  10052  fin1a2lem10  10300  trclublem  14902  trclubi  14903  trclub  14905  reltrclfv  14924  modfsummods  15700  cvgcmpce  15725  mreexexlem3d  17552  dprd2da  19957  dpjcntz  19967  dpjdisj  19968  dpjlsm  19969  dpjidcl  19973  ablfac1eu  19988  perfcls  23281  dfconn2  23335  comppfsc  23448  llycmpkgen2  23466  trfil2  23803  fixufil  23838  tsmsres  24060  ustssco  24131  ustuqtop1  24157  xrge0gsumle  24750  volsup  25485  mbfss  25575  itg2cnlem2  25691  iblss2  25735  vieta1lem2  26247  amgm  26929  wilthlem2  27007  ftalem3  27013  rpvmasum2  27451  noetalem1  27681  madeoldsuc  27831  iuninc  32538  pmtrcnel  33056  pmtrcnelor  33058  hgt750lemb  34667  rankaltopb  36019  hfun  36218  bj-prmoore  37155  nacsfix  42751  cantnfresb  43363  omabs2  43371  onsucunipr  43411  oaun2  43420  oaun3  43421  fvnonrel  43636  rclexi  43654  rtrclex  43656  trclubgNEW  43657  trclubNEW  43658  dfrtrcl5  43668  trrelsuperrel2dg  43710  iunrelexp0  43741  corcltrcl  43778  isotone1  44087  aacllem  49839