Theorem ssequn1 4139

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922

This theorem is referenced by:  ssequn2  4142  undif  4435  uniop  5462  pwssun  5515  cnvimassrndm  6105  unisucg  6391  ordssun  6415  ordequn  6416  onunel  6418  onun2  6421  funiunfv  7188  sorpssun  7670  ordunpr  7765  onuninsuci  7780  omun  7828  domss2  9060  findcard2s  9089  sucdom2  9127  rankopb  9767  ranksuc  9780  kmlem11  10074  fin1a2lem10  10322  trclublem  14920  trclubi  14921  trclub  14923  reltrclfv  14942  modfsummods  15718  cvgcmpce  15743  mreexexlem3d  17570  dprd2da  19941  dpjcntz  19951  dpjdisj  19952  dpjlsm  19953  dpjidcl  19957  ablfac1eu  19972  perfcls  23268  dfconn2  23322  comppfsc  23435  llycmpkgen2  23453  trfil2  23790  fixufil  23825  tsmsres  24047  ustssco  24118  ustuqtop1  24145  xrge0gsumle  24738  volsup  25473  mbfss  25563  itg2cnlem2  25679  iblss2  25723  vieta1lem2  26235  amgm  26917  wilthlem2  26995  ftalem3  27001  rpvmasum2  27439  noetalem1  27669  madeoldsuc  27817  iuninc  32522  pmtrcnel  33044  pmtrcnelor  33046  hgt750lemb  34626  rankaltopb  35955  hfun  36154  bj-prmoore  37091  nacsfix  42688  cantnfresb  43300  omabs2  43308  onsucunipr  43348  oaun2  43357  oaun3  43358  fvnonrel  43573  rclexi  43591  rtrclex  43593  trclubgNEW  43594  trclubNEW  43595  dfrtrcl5  43605  trrelsuperrel2dg  43647  iunrelexp0  43678  corcltrcl  43715  isotone1  44024  aacllem  49790