Theorem ssequn1 4140

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 225	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 964	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4108	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 341	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1849	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3923	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2756	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860  ∀wal 1568   = wceq 1570   ∈ wcel 2143   ∪ cun 3904   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-ss 3923

This theorem is referenced by:  ssequn2  4143  undif  4444  uniop  5500  pwssun  5555  cnvimassrndm  6151  unisucg  6443  ordssun  6467  ordequn  6468  onunel  6470  onun2  6473  funiunfv  7248  sorpssun  7729  ordunpr  7823  onuninsuci  7837  omun  7885  domss2  9125  findcard2s  9151  sucdom2  9188  rankopb  9825  ranksuc  9838  kmlem11  10145  fin1a2lem10  10394  trclublem  15034  trclubi  15035  trclub  15037  reltrclfv  15056  modfsummods  15847  cvgcmpce  15872  mreexexlem3d  17703  dprd2da  20115  dpjcntz  20125  dpjdisj  20126  dpjlsm  20127  dpjidcl  20131  ablfac1eu  20146  perfcls  23503  dfconn2  23557  comppfsc  23670  llycmpkgen2  23688  trfil2  24025  fixufil  24060  tsmsres  24282  ustssco  24353  ustuqtop1  24379  xrge0gsumle  24972  volsup  25696  mbfss  25786  itg2cnlem2  25902  iblss2  25946  vieta1lem2  26453  amgm  27136  wilthlem2  27214  ftalem3  27220  rpvmasum2  27657  noetalem1  27886  madeoldsuc  28059  iuninc  32886  pmtrcnel  33390  pmtrcnelor  33392  hgt750lemb  35024  rankaltopb  36452  hfun  36651  bj-prmoore  37738  nacsfix  43426  cantnfresb  44034  omabs2  44042  onsucunipr  44082  oaun2  44091  oaun3  44092  fvnonrel  44306  rclexi  44324  rtrclex  44326  trclubgNEW  44327  trclubNEW  44328  dfrtrcl5  44338  trrelsuperrel2dg  44380  iunrelexp0  44411  corcltrcl  44448  isotone1  44757  aacllem  50584