Theorem ssequn1 4138

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 224	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 962	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4106	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 340	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 305	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1838	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3921	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2754	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 858  ∀wal 1557   = wceq 1559   ∈ wcel 2141   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921

This theorem is referenced by:  ssequn2  4141  undif  4435  uniop  5483  pwssun  5537  cnvimassrndm  6134  unisucg  6422  ordssun  6446  ordequn  6447  onunel  6449  onun2  6452  funiunfv  7228  sorpssun  7709  ordunpr  7802  onuninsuci  7816  omun  7864  domss2  9104  findcard2s  9130  sucdom2  9167  rankopb  9807  ranksuc  9820  kmlem11  10114  fin1a2lem10  10363  trclublem  15005  trclubi  15006  trclub  15008  reltrclfv  15027  modfsummods  15804  cvgcmpce  15829  mreexexlem3d  17661  dprd2da  20067  dpjcntz  20077  dpjdisj  20078  dpjlsm  20079  dpjidcl  20083  ablfac1eu  20098  perfcls  23405  dfconn2  23459  comppfsc  23572  llycmpkgen2  23590  trfil2  23927  fixufil  23962  tsmsres  24184  ustssco  24255  ustuqtop1  24281  xrge0gsumle  24874  volsup  25598  mbfss  25688  itg2cnlem2  25804  iblss2  25848  vieta1lem2  26352  amgm  27032  wilthlem2  27110  ftalem3  27116  rpvmasum2  27553  noetalem1  27782  madeoldsuc  27955  iuninc  32709  pmtrcnel  33230  pmtrcnelor  33232  hgt750lemb  34914  rankaltopb  36293  hfun  36492  bj-prmoore  37569  nacsfix  43257  cantnfresb  43865  omabs2  43873  onsucunipr  43913  oaun2  43922  oaun3  43923  fvnonrel  44137  rclexi  44155  rtrclex  44157  trclubgNEW  44158  trclubNEW  44159  dfrtrcl5  44169  trrelsuperrel2dg  44211  iunrelexp0  44242  corcltrcl  44279  isotone1  44588  aacllem  50386