Theorem ssequn2 4138

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 4135	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4108	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2767	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∪ cun 3900   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-ss 3919

This theorem is used by:  unabs  4214  undifr  4442  tppreqb  4771  pwssun  5551  cnvimassrndm  6147  relresfldOLD  6278  ordssun  6466  ordequn  6467  onunel  6469  onun2  6472  oneluni  6482  fsnunf  7187  sorpssun  7735  ordunpr  7826  omun  7888  fodomr  9130  unfi  9169  enp1ilem  9252  pwfilem  9291  fodomfir  9301  brwdom2  9549  sucprcreg  9582  sucprcregOLD  9583  dfacfin7  10405  hashbclem  14521  incexclem  15929  ramub1lem1  17124  ramub1lem2  17125  mreexmrid  17737  lspun0  21201  lbsextlem4  21354  cldlp  23381  ordtuni  23421  lfinun  23757  cldsubg  24343  trust  24461  nulmbl2  25770  limcmpt2  26118  cnplimc  26121  dvreslem  26143  dvaddbr  26172  dvmulbr  26173  lhop  26250  plypf1  26445  coeeulem  26457  coeeu  26458  coef2  26464  rlimcnp  27210  noetalem1  27985  addsproplem2  28243  ex-un  30912  shs0i  31938  chj0i  31944  disjun0  33076  ffsrn  33207  difioo  33261  symgcom2  33532  eulerpartlemt  34890  fineqvac  35650  subfacp1lem1  35766  cvmscld  35860  mthmpps  36169  refssfne  36985  topjoin  36992  pibt2  38179  poimirlem3  38380  poimirlem28  38405  rntrclfvOAI  43544  istopclsd  43553  nacsfix  43565  diophrw  43612  tfsconcatb0  44193  onsucunipr  44221  oaun3  44231  clcnvlem  44471  cnvrcl0  44473  dmtrcl  44475  rntrcl  44476  iunrelexp0  44550  dmtrclfvRP  44578  rntrclfv  44580  cotrclrcl  44590  clsk3nimkb  44888  limciccioolb  46459  limcicciooub  46473  ioccncflimc  46721  icocncflimc  46725  stoweidlem44  46880  dirkercncflem3  46941  fourierdlem62  47004  ismeannd  47303  cycl3grtri  48871