Theorem ssequn1 4110

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 4079	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 338	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 302	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1823	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3903	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2731	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 302	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  ssequn2  4113  undif  4412  uniop  5423  pwssun  5476  cnvimassrndm  6044  unisuc  6327  ordssun  6350  ordequn  6351  onun2  6355  funiunfv  7103  sorpssun  7561  ordunpr  7648  onuninsuci  7662  sucdom2  8822  domss2  8872  findcard2s  8910  rankopb  9541  ranksuc  9554  kmlem11  9847  fin1a2lem10  10096  trclublem  14634  trclubi  14635  trclub  14637  reltrclfv  14656  modfsummods  15433  cvgcmpce  15458  mreexexlem3d  17272  dprd2da  19560  dpjcntz  19570  dpjdisj  19571  dpjlsm  19572  dpjidcl  19576  ablfac1eu  19591  perfcls  22424  dfconn2  22478  comppfsc  22591  llycmpkgen2  22609  trfil2  22946  fixufil  22981  tsmsres  23203  ustssco  23274  ustuqtop1  23301  xrge0gsumle  23902  volsup  24625  mbfss  24715  itg2cnlem2  24832  iblss2  24875  vieta1lem2  25376  amgm  26045  wilthlem2  26123  ftalem3  26129  rpvmasum2  26565  iuninc  30801  pmtrcnel  31260  pmtrcnelor  31262  hgt750lemb  32536  onunel  33592  noetalem1  33871  madeoldsuc  33994  rankaltopb  34208  hfun  34407  bj-prmoore  35213  nacsfix  40450  fvnonrel  41094  rclexi  41112  rtrclex  41114  trclubgNEW  41115  trclubNEW  41116  dfrtrcl5  41126  trrelsuperrel2dg  41168  iunrelexp0  41199  corcltrcl  41236  isotone1  41547  aacllem  46391