Theorem ssequn1 4158

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 946	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4127	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 341	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 305	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1820	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3957	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2817	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 305	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 843  ∀wal 1535   = wceq 1537   ∈ wcel 2114   ∪ cun 3936   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954

This theorem is referenced by:  ssequn2  4161  undif  4432  uniop  5407  pwssun  5458  unisuc  6269  ordssun  6292  ordequn  6293  onun2i  6308  funiunfv  7009  sorpssun  7458  ordunpr  7543  onuninsuci  7557  domss2  8678  sucdom2  8716  findcard2s  8761  rankopb  9283  ranksuc  9296  kmlem11  9588  fin1a2lem10  9833  trclublem  14357  trclubi  14358  trclub  14360  reltrclfv  14379  modfsummods  15150  cvgcmpce  15175  mreexexlem3d  16919  dprd2da  19166  dpjcntz  19176  dpjdisj  19177  dpjlsm  19178  dpjidcl  19182  ablfac1eu  19197  perfcls  21975  dfconn2  22029  comppfsc  22142  llycmpkgen2  22160  trfil2  22497  fixufil  22532  tsmsres  22754  ustssco  22825  ustuqtop1  22852  xrge0gsumle  23443  volsup  24159  mbfss  24249  itg2cnlem2  24365  iblss2  24408  vieta1lem2  24902  amgm  25570  wilthlem2  25648  ftalem3  25654  rpvmasum2  26090  iuninc  30314  pmtrcnel  30735  pmtrcnelor  30737  hgt750lemb  31929  rankaltopb  33442  hfun  33641  bj-prmoore  34409  nacsfix  39316  fvnonrel  39964  rclexi  39982  rtrclex  39984  trclubgNEW  39985  trclubNEW  39986  dfrtrcl5  39996  trrelsuperrel2dg  40023  iunrelexp0  40054  corcltrcl  40091  isotone1  40405  aacllem  44909