Theorem ssequn1 4141

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 4109	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 341	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1842	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3924	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2758	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860  ∀wal 1561   = wceq 1563   ∈ wcel 2145   ∪ cun 3905   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-ss 3924

This theorem is referenced by:  ssequn2  4144  undif  4439  uniop  5488  pwssun  5543  cnvimassrndm  6140  unisucg  6430  ordssun  6454  ordequn  6455  onunel  6457  onun2  6460  funiunfv  7236  sorpssun  7717  ordunpr  7810  onuninsuci  7824  omun  7872  domss2  9112  findcard2s  9138  sucdom2  9175  rankopb  9812  ranksuc  9825  kmlem11  10132  fin1a2lem10  10381  trclublem  15020  trclubi  15021  trclub  15023  reltrclfv  15042  modfsummods  15833  cvgcmpce  15858  mreexexlem3d  17690  dprd2da  20102  dpjcntz  20112  dpjdisj  20113  dpjlsm  20114  dpjidcl  20118  ablfac1eu  20133  perfcls  23479  dfconn2  23533  comppfsc  23646  llycmpkgen2  23664  trfil2  24001  fixufil  24036  tsmsres  24258  ustssco  24329  ustuqtop1  24355  xrge0gsumle  24948  volsup  25672  mbfss  25762  itg2cnlem2  25878  iblss2  25922  vieta1lem2  26429  amgm  27109  wilthlem2  27187  ftalem3  27193  rpvmasum2  27630  noetalem1  27859  madeoldsuc  28032  iuninc  32811  pmtrcnel  33317  pmtrcnelor  33319  hgt750lemb  34955  rankaltopb  36337  hfun  36536  bj-prmoore  37612  nacsfix  43300  cantnfresb  43908  omabs2  43916  onsucunipr  43956  oaun2  43965  oaun3  43966  fvnonrel  44180  rclexi  44198  rtrclex  44200  trclubgNEW  44201  trclubNEW  44202  dfrtrcl5  44212  trrelsuperrel2dg  44254  iunrelexp0  44285  corcltrcl  44322  isotone1  44631  aacllem  50431