Theorem ssequn1 4196

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1535   = wceq 1537   ∈ wcel 2106   ∪ cun 3961   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980

This theorem is referenced by:  ssequn2  4199  undif  4488  uniop  5525  pwssun  5580  cnvimassrndm  6174  unisucg  6464  ordssun  6488  ordequn  6489  onunel  6491  onun2  6494  funiunfv  7268  sorpssun  7749  ordunpr  7846  onuninsuci  7861  omun  7910  sucdom2OLD  9121  domss2  9175  findcard2s  9204  sucdom2  9241  rankopb  9890  ranksuc  9903  kmlem11  10199  fin1a2lem10  10447  trclublem  15031  trclubi  15032  trclub  15034  reltrclfv  15053  modfsummods  15826  cvgcmpce  15851  mreexexlem3d  17691  dprd2da  20077  dpjcntz  20087  dpjdisj  20088  dpjlsm  20089  dpjidcl  20093  ablfac1eu  20108  perfcls  23389  dfconn2  23443  comppfsc  23556  llycmpkgen2  23574  trfil2  23911  fixufil  23946  tsmsres  24168  ustssco  24239  ustuqtop1  24266  xrge0gsumle  24869  volsup  25605  mbfss  25695  itg2cnlem2  25812  iblss2  25856  vieta1lem2  26368  amgm  27049  wilthlem2  27127  ftalem3  27133  rpvmasum2  27571  noetalem1  27801  madeoldsuc  27938  iuninc  32581  pmtrcnel  33092  pmtrcnelor  33094  hgt750lemb  34650  rankaltopb  35961  hfun  36160  bj-prmoore  37098  nacsfix  42700  cantnfresb  43314  omabs2  43322  onsucunipr  43362  oaun2  43371  oaun3  43372  fvnonrel  43587  rclexi  43605  rtrclex  43607  trclubgNEW  43608  trclubNEW  43609  dfrtrcl5  43619  trrelsuperrel2dg  43661  iunrelexp0  43692  corcltrcl  43729  isotone1  44038  aacllem  49032