Theorem ssequn1 4135

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1539   = wceq 1541   ∈ wcel 2113   ∪ cun 3896   ⊆ wss 3898

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  ssequn2  4138  undif  4431  uniop  5460  pwssun  5513  cnvimassrndm  6106  unisucg  6393  ordssun  6417  ordequn  6418  onunel  6420  onun2  6423  funiunfv  7190  sorpssun  7671  ordunpr  7764  onuninsuci  7778  omun  7826  domss2  9058  findcard2s  9084  sucdom2  9121  rankopb  9754  ranksuc  9767  kmlem11  10061  fin1a2lem10  10309  trclublem  14906  trclubi  14907  trclub  14909  reltrclfv  14928  modfsummods  15704  cvgcmpce  15729  mreexexlem3d  17556  dprd2da  19960  dpjcntz  19970  dpjdisj  19971  dpjlsm  19972  dpjidcl  19976  ablfac1eu  19991  perfcls  23283  dfconn2  23337  comppfsc  23450  llycmpkgen2  23468  trfil2  23805  fixufil  23840  tsmsres  24062  ustssco  24133  ustuqtop1  24159  xrge0gsumle  24752  volsup  25487  mbfss  25577  itg2cnlem2  25693  iblss2  25737  vieta1lem2  26249  amgm  26931  wilthlem2  27009  ftalem3  27015  rpvmasum2  27453  noetalem1  27683  madeoldsuc  27833  iuninc  32544  pmtrcnel  33067  pmtrcnelor  33069  hgt750lemb  34692  rankaltopb  36046  hfun  36245  bj-prmoore  37182  nacsfix  42832  cantnfresb  43444  omabs2  43452  onsucunipr  43492  oaun2  43501  oaun3  43502  fvnonrel  43717  rclexi  43735  rtrclex  43737  trclubgNEW  43738  trclubNEW  43739  dfrtrcl5  43749  trrelsuperrel2dg  43791  iunrelexp0  43822  corcltrcl  43859  isotone1  44168  aacllem  49929