Theorem ssequn1 4166

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 222	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 951	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4133	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 338	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 303	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1819	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3948	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2729	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109   ∪ cun 3929   ⊆ wss 3931

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  ssequn2  4169  undif  4462  uniop  5495  pwssun  5550  cnvimassrndm  6146  unisucg  6437  ordssun  6461  ordequn  6462  onunel  6464  onun2  6467  funiunfv  7245  sorpssun  7729  ordunpr  7825  onuninsuci  7840  omun  7888  sucdom2OLD  9101  domss2  9155  findcard2s  9184  sucdom2  9222  rankopb  9871  ranksuc  9884  kmlem11  10180  fin1a2lem10  10428  trclublem  15019  trclubi  15020  trclub  15022  reltrclfv  15041  modfsummods  15814  cvgcmpce  15839  mreexexlem3d  17663  dprd2da  20030  dpjcntz  20040  dpjdisj  20041  dpjlsm  20042  dpjidcl  20046  ablfac1eu  20061  perfcls  23308  dfconn2  23362  comppfsc  23475  llycmpkgen2  23493  trfil2  23830  fixufil  23865  tsmsres  24087  ustssco  24158  ustuqtop1  24185  xrge0gsumle  24778  volsup  25514  mbfss  25604  itg2cnlem2  25720  iblss2  25764  vieta1lem2  26276  amgm  26958  wilthlem2  27036  ftalem3  27042  rpvmasum2  27480  noetalem1  27710  madeoldsuc  27853  iuninc  32546  pmtrcnel  33105  pmtrcnelor  33107  hgt750lemb  34693  rankaltopb  36002  hfun  36201  bj-prmoore  37138  nacsfix  42710  cantnfresb  43323  omabs2  43331  onsucunipr  43371  oaun2  43380  oaun3  43381  fvnonrel  43596  rclexi  43614  rtrclex  43616  trclubgNEW  43617  trclubNEW  43618  dfrtrcl5  43628  trrelsuperrel2dg  43670  iunrelexp0  43701  corcltrcl  43738  isotone1  44047  aacllem  49645