Theorem ssequn2 4190

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  unabs  4213  undifr  4442  tppreqb  4768  pwssun  5547  cnvimassrndmOLD  6212  imadifssrn  6214  relresfldOLD  6297  ordssun  6485  ordequn  6486  onunel  6488  onun2  6491  oneluni  6501  fsnunf  7213  sorpssun  7770  ordunpr  7861  omun  7923  fodomr  9175  unfi  9214  enp1ilem  9297  pwfilem  9337  fodomfir  9347  brwdom2  9594  sucprcreg  9627  sucprcregOLD  9628  dfacfin7  10504  hashbclem  14624  incexclem  16034  ramub1lem1  17233  ramub1lem2  17234  mreexmrid  17846  lspun0  21316  lbsextlem4  21469  cldlp  23498  ordtuni  23538  lfinun  23874  cldsubg  24460  trust  24578  nulmbl2  25887  limcmpt2  26234  cnplimc  26237  dvreslem  26259  dvaddbr  26288  dvmulbr  26289  lhop  26366  plypf1  26561  coeeulem  26573  coeeu  26574  coef2  26580  rlimcnp  27323  noetalem1  28128  addsproplem2  28386  ex-un  31055  shs0i  32081  chj0i  32087  disjun0  33261  ffsrn  33390  difioo  33444  symgcom2  33715  eulerpartlemt  35073  ordunmax  35792  fineqvac  35884  subfacp1lem1  36111  cvmscld  36205  mthmpps  36514  refssfne  37324  topjoin  37331  pibt2  38532  poimirlem3  38733  poimirlem28  38758  rntrclfvOAI  43895  istopclsd  43904  nacsfix  43916  diophrw  43963  tfsconcatb0  44538  onsucunipr  44566  oaun3  44576  clcnvlem  44815  cnvrcl0  44817  dmtrcl  44819  rntrcl  44820  iunrelexp0  44894  dmtrclfvRP  44922  rntrclfv  44924  cotrclrcl  44934  clsk3nimkb  45232  limciccioolb  46838  limcicciooub  46852  ioccncflimc  47100  icocncflimc  47104  stoweidlem44  47259  dirkercncflem3  47320  fourierdlem62  47383  ismeannd  47682  cycl3grtri  49250