Theorem ssequn1 3783

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 212	. . . 4 ⊢ ((𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
2		pm4.72 920	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 3753	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 328	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 292	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1747	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3591	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2616	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383  ∀wal 1481   = wceq 1483   ∈ wcel 1990   ∪ cun 3572   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  ssequn2  3786  undif  4049  uniop  4977  pwssun  5020  unisuc  5801  ordssun  5827  ordequn  5828  onun2i  5843  funiunfv  6506  sorpssun  6944  ordunpr  7026  onuninsuci  7040  domss2  8119  sucdom2  8156  findcard2s  8201  rankopb  8715  ranksuc  8728  kmlem11  8982  fin1a2lem10  9231  trclublem  13734  trclubi  13735  trclubiOLD  13736  trclub  13739  reltrclfv  13758  modfsummods  14525  cvgcmpce  14550  mreexexlem3d  16306  dprd2da  18441  dpjcntz  18451  dpjdisj  18452  dpjlsm  18453  dpjidcl  18457  ablfac1eu  18472  perfcls  21169  dfconn2  21222  comppfsc  21335  llycmpkgen2  21353  trfil2  21691  fixufil  21726  tsmsres  21947  ustssco  22018  ustuqtop1  22045  xrge0gsumle  22636  volsup  23324  mbfss  23413  itg2cnlem2  23529  iblss2  23572  vieta1lem2  24066  amgm  24717  wilthlem2  24795  ftalem3  24801  rpvmasum2  25201  iuninc  29379  hgt750lemb  30734  rankaltopb  32086  hfun  32285  nacsfix  37275  fvnonrel  37903  rclexi  37922  rtrclex  37924  trclubgNEW  37925  trclubNEW  37926  dfrtrcl5  37936  trrelsuperrel2dg  37963  iunrelexp0  37994  corcltrcl  38031  isotone1  38346  aacllem  42547