Theorem ssequn2 4090

Description: A relationship between subclass and union. (Contributed by NM, 13-Jun-1994.)

Assertion

Ref	Expression
ssequn2	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Proof of Theorem ssequn2

Step	Hyp	Ref	Expression
1		ssequn1 4087	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4060	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2763	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1538   ∪ cun 3858   ⊆ wss 3860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-un 3865  df-in 3867  df-ss 3877

This theorem is referenced by:  unabs  4161  tppreqb  4698  pwssun  5429  pwundifOLD  5430  relresfld  6109  ordssun  6272  ordequn  6273  onun2  6277  oneluni  6286  fsnunf  6943  sorpssun  7459  ordunpr  7545  fodomr  8695  unfi  8746  pwfilem  8750  enp1ilem  8793  pwfilemOLD  8856  brwdom2  9075  sucprcreg  9103  dfacfin7  9864  hashbclem  13865  incexclem  15244  ramub1lem1  16422  ramub1lem2  16423  mreexmrid  16977  lspun0  19856  lbsextlem4  20006  cldlp  21855  ordtuni  21895  lfinun  22230  cldsubg  22816  trust  22935  nulmbl2  24241  limcmpt2  24588  cnplimc  24591  dvreslem  24613  dvaddbr  24642  dvmulbr  24643  lhop  24720  plypf1  24913  coeeulem  24925  coeeu  24926  coef2  24932  rlimcnp  25655  ex-un  28313  shs0i  29336  chj0i  29342  disjun0  30461  ffsrn  30592  difioo  30631  symgcom2  30883  eulerpartlemt  31861  subfacp1lem1  32661  cvmscld  32755  mthmpps  33064  noetalem1  33533  refssfne  34122  topjoin  34129  pibt2  35140  poimirlem3  35366  poimirlem28  35391  rntrclfvOAI  40033  istopclsd  40042  nacsfix  40054  diophrw  40101  clcnvlem  40724  cnvrcl0  40726  dmtrcl  40728  rntrcl  40729  iunrelexp0  40804  dmtrclfvRP  40832  rntrclfv  40834  cotrclrcl  40844  clsk3nimkb  41144  limciccioolb  42657  limcicciooub  42673  ioccncflimc  42921  icocncflimc  42925  stoweidlem44  43080  dirkercncflem3  43141  fourierdlem62  43204  ismeannd  43500