Theorem ssequn1 4122

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 223	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 957	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4090	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 339	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 304	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2733	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 304	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 853  ∀wal 1545   = wceq 1547   ∈ wcel 2119   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-ss 3907

This theorem is referenced by:  ssequn2  4125  undif  4417  uniop  5463  pwssun  5517  cnvimassrndm  6110  unisucg  6397  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  funiunfv  7199  sorpssun  7680  ordunpr  7773  onuninsuci  7787  omun  7835  domss2  9071  findcard2s  9097  sucdom2  9134  rankopb  9774  ranksuc  9787  kmlem11  10081  fin1a2lem10  10329  trclublem  14955  trclubi  14956  trclub  14958  reltrclfv  14977  modfsummods  15754  cvgcmpce  15779  mreexexlem3d  17610  dprd2da  20017  dpjcntz  20027  dpjdisj  20028  dpjlsm  20029  dpjidcl  20033  ablfac1eu  20048  perfcls  23355  dfconn2  23409  comppfsc  23522  llycmpkgen2  23540  trfil2  23877  fixufil  23912  tsmsres  24134  ustssco  24205  ustuqtop1  24231  xrge0gsumle  24824  volsup  25548  mbfss  25638  itg2cnlem2  25754  iblss2  25798  vieta1lem2  26302  amgm  26979  wilthlem2  27057  ftalem3  27063  rpvmasum2  27500  noetalem1  27730  madeoldsuc  27902  iuninc  32656  pmtrcnel  33177  pmtrcnelor  33179  hgt750lemb  34847  rankaltopb  36214  hfun  36413  bj-prmoore  37480  nacsfix  43168  cantnfresb  43776  omabs2  43784  onsucunipr  43824  oaun2  43833  oaun3  43834  fvnonrel  44048  rclexi  44066  rtrclex  44068  trclubgNEW  44069  trclubNEW  44070  dfrtrcl5  44080  trrelsuperrel2dg  44122  iunrelexp0  44153  corcltrcl  44190  isotone1  44499  aacllem  50298