Theorem ssequn1 4132

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861  ∀wal 1568   = wceq 1570   ∈ wcel 2145   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  ssequn2  4135  undif  4438  uniop  5488  pwssun  5543  cnvimassrndm  6141  unisucg  6436  ordssun  6460  ordequn  6461  onunel  6463  onun2  6466  funiunfv  7244  sorpssun  7735  ordunpr  7826  onuninsuci  7840  omun  7888  domss2  9139  findcard2s  9165  sucdom2  9202  rankopb  9847  ranksuc  9863  hfunOLD  9900  kmlem11  10220  fin1a2lem10  10468  trclublem  15128  trclubi  15129  trclub  15131  reltrclfv  15150  modfsummods  15940  cvgcmpce  15965  mreexexlem3d  17800  dprd2da  20238  dpjcntz  20248  dpjdisj  20249  dpjlsm  20250  dpjidcl  20254  ablfac1eu  20269  perfcls  23663  dfconn2  23717  comppfsc  23831  llycmpkgen2  23849  trfil2  24186  fixufil  24221  tsmsres  24443  ustssco  24514  ustuqtop1  24540  xrge0gsumle  25133  volsup  25857  mbfss  25947  itg2cnlem2  26063  iblss2  26106  vieta1lem2  26616  amgm  27300  wilthlem2  27378  ftalem3  27384  rpvmasum2  27821  noetalem1  28080  madeoldsuc  28253  iuninc  33137  pmtrcnel  33632  pmtrcnelor  33634  hgt750lemb  35268  rankaltopb  36714  bj-prmoore  38004  nacsfix  43676  cantnfresb  44284  omabs2  44292  onsucunipr  44332  oaun2  44341  oaun3  44342  fvnonrel  44556  rclexi  44574  rtrclex  44576  trclubgNEW  44577  trclubNEW  44578  dfrtrcl5  44588  trrelsuperrel2dg  44630  iunrelexp0  44661  corcltrcl  44698  isotone1  45007  tmachlem-agreeprod  47891  aacllem  50883