Theorem ssequn1 4126

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 952	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 4093	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 338	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 303	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1821	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		df-ss 3906	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2729	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 303	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848  ∀wal 1540   = wceq 1542   ∈ wcel 2114   ∪ cun 3887   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906

This theorem is referenced by:  ssequn2  4129  undif  4422  uniop  5469  pwssun  5523  cnvimassrndm  6116  unisucg  6403  ordssun  6427  ordequn  6428  onunel  6430  onun2  6433  funiunfv  7203  sorpssun  7684  ordunpr  7777  onuninsuci  7791  omun  7839  domss2  9074  findcard2s  9100  sucdom2  9137  rankopb  9776  ranksuc  9789  kmlem11  10083  fin1a2lem10  10331  trclublem  14957  trclubi  14958  trclub  14960  reltrclfv  14979  modfsummods  15756  cvgcmpce  15781  mreexexlem3d  17612  dprd2da  20019  dpjcntz  20029  dpjdisj  20030  dpjlsm  20031  dpjidcl  20035  ablfac1eu  20050  perfcls  23330  dfconn2  23384  comppfsc  23497  llycmpkgen2  23515  trfil2  23852  fixufil  23887  tsmsres  24109  ustssco  24180  ustuqtop1  24206  xrge0gsumle  24799  volsup  25523  mbfss  25613  itg2cnlem2  25729  iblss2  25773  vieta1lem2  26277  amgm  26954  wilthlem2  27032  ftalem3  27038  rpvmasum2  27475  noetalem1  27705  madeoldsuc  27877  iuninc  32630  pmtrcnel  33150  pmtrcnelor  33152  hgt750lemb  34800  rankaltopb  36161  hfun  36360  bj-prmoore  37427  nacsfix  43144  cantnfresb  43752  omabs2  43760  onsucunipr  43800  oaun2  43809  oaun3  43810  fvnonrel  44024  rclexi  44042  rtrclex  44044  trclubgNEW  44045  trclubNEW  44046  dfrtrcl5  44056  trrelsuperrel2dg  44098  iunrelexp0  44129  corcltrcl  44166  isotone1  44475  aacllem  50276