Theorem ssequn1 4185

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847  ∀wal 1537   = wceq 1539   ∈ wcel 2107   ∪ cun 3948   ⊆ wss 3950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-un 3955  df-ss 3967

This theorem is referenced by:  ssequn2  4188  undif  4481  uniop  5519  pwssun  5574  cnvimassrndm  6171  unisucg  6461  ordssun  6485  ordequn  6486  onunel  6488  onun2  6491  funiunfv  7269  sorpssun  7751  ordunpr  7847  onuninsuci  7862  omun  7910  sucdom2OLD  9123  domss2  9177  findcard2s  9206  sucdom2  9244  rankopb  9893  ranksuc  9906  kmlem11  10202  fin1a2lem10  10450  trclublem  15035  trclubi  15036  trclub  15038  reltrclfv  15057  modfsummods  15830  cvgcmpce  15855  mreexexlem3d  17690  dprd2da  20063  dpjcntz  20073  dpjdisj  20074  dpjlsm  20075  dpjidcl  20079  ablfac1eu  20094  perfcls  23374  dfconn2  23428  comppfsc  23541  llycmpkgen2  23559  trfil2  23896  fixufil  23931  tsmsres  24153  ustssco  24224  ustuqtop1  24251  xrge0gsumle  24856  volsup  25592  mbfss  25682  itg2cnlem2  25798  iblss2  25842  vieta1lem2  26354  amgm  27035  wilthlem2  27113  ftalem3  27119  rpvmasum2  27557  noetalem1  27787  madeoldsuc  27924  iuninc  32574  pmtrcnel  33110  pmtrcnelor  33112  hgt750lemb  34672  rankaltopb  35981  hfun  36180  bj-prmoore  37117  nacsfix  42728  cantnfresb  43342  omabs2  43350  onsucunipr  43390  oaun2  43399  oaun3  43400  fvnonrel  43615  rclexi  43633  rtrclex  43635  trclubgNEW  43636  trclubNEW  43637  dfrtrcl5  43647  trrelsuperrel2dg  43689  iunrelexp0  43720  corcltrcl  43757  isotone1  44066  aacllem  49375