Theorem ssequn1 3891

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 956	. . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ 𝐵 ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵)))
3		elun 3861	. . . . 5 ⊢ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ (𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵))
4	3	bibi1i 327	. . . 4 ⊢ ((𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵) ↔ ((𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵) ↔ 𝑥 ∈ 𝐵))
5	1, 2, 4	3bitr4i 292	. . 3 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ (𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
6	5	albii 1860	. 2 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
7		dfss2 3697	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
8		dfcleq 2718	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ ∀𝑥(𝑥 ∈ (𝐴 ∪ 𝐵) ↔ 𝑥 ∈ 𝐵))
9	6, 7, 8	3bitr4i 292	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382  ∀wal 1594   = wceq 1596   ∈ wcel 2103   ∪ cun 3678   ⊆ wss 3680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-v 3306  df-un 3685  df-in 3687  df-ss 3694

This theorem is referenced by:  ssequn2  3894  undif  4157  uniop  5081  pwssun  5124  unisuc  5914  ordssun  5940  ordequn  5941  onun2i  5956  funiunfv  6621  sorpssun  7061  ordunpr  7143  onuninsuci  7157  domss2  8235  sucdom2  8272  findcard2s  8317  rankopb  8828  ranksuc  8841  kmlem11  9095  fin1a2lem10  9344  trclublem  13856  trclubi  13857  trclub  13859  reltrclfv  13878  modfsummods  14645  cvgcmpce  14670  mreexexlem3d  16429  dprd2da  18562  dpjcntz  18572  dpjdisj  18573  dpjlsm  18574  dpjidcl  18578  ablfac1eu  18593  perfcls  21292  dfconn2  21345  comppfsc  21458  llycmpkgen2  21476  trfil2  21813  fixufil  21848  tsmsres  22069  ustssco  22140  ustuqtop1  22167  xrge0gsumle  22758  volsup  23445  mbfss  23533  itg2cnlem2  23649  iblss2  23692  vieta1lem2  24186  amgm  24837  wilthlem2  24915  ftalem3  24921  rpvmasum2  25321  iuninc  29607  hgt750lemb  30964  rankaltopb  32313  hfun  32512  nacsfix  37694  fvnonrel  38322  rclexi  38341  rtrclex  38343  trclubgNEW  38344  trclubNEW  38345  dfrtrcl5  38355  trrelsuperrel2dg  38382  iunrelexp0  38413  corcltrcl  38450  isotone1  38765  aacllem  42977