Theorem ssequn1 4127

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

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  ssequn2  4130  undif  4423  uniop  5461  pwssun  5514  cnvimassrndm  6108  unisucg  6395  ordssun  6419  ordequn  6420  onunel  6422  onun2  6425  funiunfv  7194  sorpssun  7675  ordunpr  7768  onuninsuci  7782  omun  7830  domss2  9065  findcard2s  9091  sucdom2  9128  rankopb  9765  ranksuc  9778  kmlem11  10072  fin1a2lem10  10320  trclublem  14946  trclubi  14947  trclub  14949  reltrclfv  14968  modfsummods  15745  cvgcmpce  15770  mreexexlem3d  17601  dprd2da  20008  dpjcntz  20018  dpjdisj  20019  dpjlsm  20020  dpjidcl  20024  ablfac1eu  20039  perfcls  23339  dfconn2  23393  comppfsc  23506  llycmpkgen2  23524  trfil2  23861  fixufil  23896  tsmsres  24118  ustssco  24189  ustuqtop1  24215  xrge0gsumle  24808  volsup  25532  mbfss  25622  itg2cnlem2  25738  iblss2  25782  vieta1lem2  26290  amgm  26972  wilthlem2  27050  ftalem3  27056  rpvmasum2  27494  noetalem1  27724  madeoldsuc  27896  iuninc  32650  pmtrcnel  33170  pmtrcnelor  33172  hgt750lemb  34821  rankaltopb  36182  hfun  36381  bj-prmoore  37440  nacsfix  43155  cantnfresb  43767  omabs2  43775  onsucunipr  43815  oaun2  43824  oaun3  43825  fvnonrel  44039  rclexi  44057  rtrclex  44059  trclubgNEW  44060  trclubNEW  44061  dfrtrcl5  44071  trrelsuperrel2dg  44113  iunrelexp0  44144  corcltrcl  44181  isotone1  44490  aacllem  50273