Theorem ssequn1 4114

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 221	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 947	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4083	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 339	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 303	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1822	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3907	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2731	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 844  ∀wal 1537   = wceq 1539   ∈ wcel 2106   ∪ cun 3885   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904

This theorem is referenced by:  ssequn2  4117  undif  4415  uniop  5429  pwssun  5485  cnvimassrndm  6055  unisuc  6342  ordssun  6365  ordequn  6366  onun2  6370  funiunfv  7121  sorpssun  7583  ordunpr  7673  onuninsuci  7687  sucdom2OLD  8869  domss2  8923  findcard2s  8948  sucdom2  8989  rankopb  9610  ranksuc  9623  kmlem11  9916  fin1a2lem10  10165  trclublem  14706  trclubi  14707  trclub  14709  reltrclfv  14728  modfsummods  15505  cvgcmpce  15530  mreexexlem3d  17355  dprd2da  19645  dpjcntz  19655  dpjdisj  19656  dpjlsm  19657  dpjidcl  19661  ablfac1eu  19676  perfcls  22516  dfconn2  22570  comppfsc  22683  llycmpkgen2  22701  trfil2  23038  fixufil  23073  tsmsres  23295  ustssco  23366  ustuqtop1  23393  xrge0gsumle  23996  volsup  24720  mbfss  24810  itg2cnlem2  24927  iblss2  24970  vieta1lem2  25471  amgm  26140  wilthlem2  26218  ftalem3  26224  rpvmasum2  26660  iuninc  30900  pmtrcnel  31358  pmtrcnelor  31360  hgt750lemb  32636  onunel  33689  noetalem1  33944  madeoldsuc  34067  rankaltopb  34281  hfun  34480  bj-prmoore  35286  nacsfix  40534  nlimsuc  41048  fvnonrel  41205  rclexi  41223  rtrclex  41225  trclubgNEW  41226  trclubNEW  41227  dfrtrcl5  41237  trrelsuperrel2dg  41279  iunrelexp0  41310  corcltrcl  41347  isotone1  41658  aacllem  46505