Theorem ssequn1 4179

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 946	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4147	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 337	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 302	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3967	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2723	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843  ∀wal 1537   = wceq 1539   ∈ wcel 2104   ∪ cun 3945   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-in 3954  df-ss 3964

This theorem is referenced by:  ssequn2  4182  undif  4480  uniop  5514  pwssun  5570  cnvimassrndm  6150  unisucg  6441  ordssun  6465  ordequn  6466  onunel  6468  onun2  6471  funiunfv  7249  sorpssun  7722  ordunpr  7816  onuninsuci  7831  omun  7880  sucdom2OLD  9084  domss2  9138  findcard2s  9167  sucdom2  9208  rankopb  9849  ranksuc  9862  kmlem11  10157  fin1a2lem10  10406  trclublem  14946  trclubi  14947  trclub  14949  reltrclfv  14968  modfsummods  15743  cvgcmpce  15768  mreexexlem3d  17594  dprd2da  19953  dpjcntz  19963  dpjdisj  19964  dpjlsm  19965  dpjidcl  19969  ablfac1eu  19984  perfcls  23089  dfconn2  23143  comppfsc  23256  llycmpkgen2  23274  trfil2  23611  fixufil  23646  tsmsres  23868  ustssco  23939  ustuqtop1  23966  xrge0gsumle  24569  volsup  25305  mbfss  25395  itg2cnlem2  25512  iblss2  25555  vieta1lem2  26060  amgm  26731  wilthlem2  26809  ftalem3  26815  rpvmasum2  27251  noetalem1  27480  madeoldsuc  27616  iuninc  32059  pmtrcnel  32520  pmtrcnelor  32522  hgt750lemb  33966  rankaltopb  35255  hfun  35454  bj-prmoore  36299  nacsfix  41752  cantnfresb  42376  omabs2  42384  onsucunipr  42424  oaun2  42433  oaun3  42434  fvnonrel  42650  rclexi  42668  rtrclex  42670  trclubgNEW  42671  trclubNEW  42672  dfrtrcl5  42682  trrelsuperrel2dg  42724  iunrelexp0  42755  corcltrcl  42792  isotone1  43101  aacllem  47935