Theorem ssequn1 3745

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 211	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 916	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 3715	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 327	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 291	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1737	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3557	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2604	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 291	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382  ∀wal 1473   = wceq 1475   ∈ wcel 1977   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  ssequn2  3748  undif  4001  uniop  4902  pwssun  4944  unisuc  5718  ordssun  5744  ordequn  5745  onun2i  5760  funiunfv  6410  sorpssun  6842  ordunpr  6918  onuninsuci  6932  domss2  8004  sucdom2  8041  findcard2s  8086  rankopb  8598  ranksuc  8611  kmlem11  8865  fin1a2lem10  9114  trclublem  13582  trclubi  13583  trclubiOLD  13584  trclub  13587  reltrclfv  13606  modfsummods  14366  cvgcmpce  14391  mreexexlem3d  16129  dprd2da  18264  dpjcntz  18274  dpjdisj  18275  dpjlsm  18276  dpjidcl  18280  ablfac1eu  18295  perfcls  20979  dfcon2  21032  comppfsc  21145  llycmpkgen2  21163  trfil2  21501  fixufil  21536  tsmsres  21757  ustssco  21828  ustuqtop1  21855  xrge0gsumle  22444  volsup  23131  mbfss  23219  itg2cnlem2  23335  iblss2  23378  vieta1lem2  23870  amgm  24517  wilthlem2  24595  ftalem3  24601  rpvmasum2  25001  iuninc  28761  rankaltopb  31256  hfun  31455  nacsfix  36293  fvnonrel  36922  rclexi  36941  rtrclex  36943  trclubgNEW  36944  trclubNEW  36945  dfrtrcl5  36955  trrelsuperrel2dg  36982  iunrelexp0  37013  corcltrcl  37050  isotone1  37366  aacllem  42356