Theorem ssequn1 4080

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 949	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4049	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 342	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 306	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1826	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3873	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2732	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 306	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 846  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∪ cun 3851   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3402  df-un 3858  df-in 3860  df-ss 3870

This theorem is referenced by:  ssequn2  4083  undif  4381  uniop  5382  pwssun  5435  cnvimassrndm  5994  unisuc  6258  ordssun  6281  ordequn  6282  onun2  6286  funiunfv  7030  sorpssun  7486  ordunpr  7572  onuninsuci  7586  sucdom2  8688  domss2  8738  findcard2s  8776  rankopb  9366  ranksuc  9379  kmlem11  9672  fin1a2lem10  9921  trclublem  14456  trclubi  14457  trclub  14459  reltrclfv  14478  modfsummods  15253  cvgcmpce  15278  mreexexlem3d  17032  dprd2da  19295  dpjcntz  19305  dpjdisj  19306  dpjlsm  19307  dpjidcl  19311  ablfac1eu  19326  perfcls  22128  dfconn2  22182  comppfsc  22295  llycmpkgen2  22313  trfil2  22650  fixufil  22685  tsmsres  22907  ustssco  22978  ustuqtop1  23005  xrge0gsumle  23597  volsup  24320  mbfss  24410  itg2cnlem2  24527  iblss2  24570  vieta1lem2  25071  amgm  25740  wilthlem2  25818  ftalem3  25824  rpvmasum2  26260  iuninc  30486  pmtrcnel  30947  pmtrcnelor  30949  hgt750lemb  32218  onunel  33275  noetalem1  33599  madeoldsuc  33722  rankaltopb  33936  hfun  34135  bj-prmoore  34939  nacsfix  40146  fvnonrel  40790  rclexi  40808  rtrclex  40810  trclubgNEW  40811  trclubNEW  40812  dfrtrcl5  40822  trrelsuperrel2dg  40865  iunrelexp0  40896  corcltrcl  40933  isotone1  41244  aacllem  46005