Theorem ssequn1 4138

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  ssequn2  4141  undif  4434  uniop  5463  pwssun  5516  cnvimassrndm  6110  unisucg  6397  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  funiunfv  7194  sorpssun  7675  ordunpr  7768  onuninsuci  7782  omun  7830  domss2  9064  findcard2s  9090  sucdom2  9127  rankopb  9764  ranksuc  9777  kmlem11  10071  fin1a2lem10  10319  trclublem  14918  trclubi  14919  trclub  14921  reltrclfv  14940  modfsummods  15716  cvgcmpce  15741  mreexexlem3d  17569  dprd2da  19973  dpjcntz  19983  dpjdisj  19984  dpjlsm  19985  dpjidcl  19989  ablfac1eu  20004  perfcls  23309  dfconn2  23363  comppfsc  23476  llycmpkgen2  23494  trfil2  23831  fixufil  23866  tsmsres  24088  ustssco  24159  ustuqtop1  24185  xrge0gsumle  24778  volsup  25513  mbfss  25603  itg2cnlem2  25719  iblss2  25763  vieta1lem2  26275  amgm  26957  wilthlem2  27035  ftalem3  27041  rpvmasum2  27479  noetalem1  27709  madeoldsuc  27881  iuninc  32635  pmtrcnel  33171  pmtrcnelor  33173  hgt750lemb  34813  rankaltopb  36173  hfun  36372  bj-prmoore  37320  nacsfix  42954  cantnfresb  43566  omabs2  43574  onsucunipr  43614  oaun2  43623  oaun3  43624  fvnonrel  43838  rclexi  43856  rtrclex  43858  trclubgNEW  43859  trclubNEW  43860  dfrtrcl5  43870  trrelsuperrel2dg  43912  iunrelexp0  43943  corcltrcl  43980  isotone1  44289  aacllem  50046