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  5463  pwssun  5516  cnvimassrndm  6110  unisucg  6397  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  funiunfv  7196  sorpssun  7677  ordunpr  7770  onuninsuci  7784  omun  7832  domss2  9067  findcard2s  9093  sucdom2  9130  rankopb  9767  ranksuc  9780  kmlem11  10074  fin1a2lem10  10322  trclublem  14948  trclubi  14949  trclub  14951  reltrclfv  14970  modfsummods  15747  cvgcmpce  15772  mreexexlem3d  17603  dprd2da  20010  dpjcntz  20020  dpjdisj  20021  dpjlsm  20022  dpjidcl  20026  ablfac1eu  20041  perfcls  23340  dfconn2  23394  comppfsc  23507  llycmpkgen2  23525  trfil2  23862  fixufil  23897  tsmsres  24119  ustssco  24190  ustuqtop1  24216  xrge0gsumle  24809  volsup  25533  mbfss  25623  itg2cnlem2  25739  iblss2  25783  vieta1lem2  26288  amgm  26968  wilthlem2  27046  ftalem3  27052  rpvmasum2  27489  noetalem1  27719  madeoldsuc  27891  iuninc  32645  pmtrcnel  33165  pmtrcnelor  33167  hgt750lemb  34816  rankaltopb  36177  hfun  36376  bj-prmoore  37443  nacsfix  43158  cantnfresb  43770  omabs2  43778  onsucunipr  43818  oaun2  43827  oaun3  43828  fvnonrel  44042  rclexi  44060  rtrclex  44062  trclubgNEW  44063  trclubNEW  44064  dfrtrcl5  44074  trrelsuperrel2dg  44116  iunrelexp0  44147  corcltrcl  44184  isotone1  44493  aacllem  50288