Theorem ssequn2 4135

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

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

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3902  df-ss 3915

This theorem is used by:  unabs  4211  undifr  4439  tppreqb  4768  pwssun  5543  cnvimassrndmOLD  6200  imadifssrn  6202  relresfldOLD  6280  ordssun  6468  ordequn  6469  onunel  6471  onun2  6474  oneluni  6484  fsnunf  7191  sorpssun  7747  ordunpr  7838  omun  7900  fodomr  9148  unfi  9187  enp1ilem  9270  pwfilem  9310  fodomfir  9320  brwdom2  9568  sucprcreg  9601  sucprcregOLD  9602  dfacfin7  10478  hashbclem  14598  incexclem  16006  ramub1lem1  17205  ramub1lem2  17206  mreexmrid  17818  lspun0  21287  lbsextlem4  21440  cldlp  23469  ordtuni  23509  lfinun  23845  cldsubg  24431  trust  24549  nulmbl2  25858  limcmpt2  26205  cnplimc  26208  dvreslem  26230  dvaddbr  26259  dvmulbr  26260  lhop  26337  plypf1  26532  coeeulem  26544  coeeu  26545  coef2  26551  rlimcnp  27294  noetalem1  28099  addsproplem2  28357  ex-un  31026  shs0i  32052  chj0i  32058  disjun0  33190  ffsrn  33321  difioo  33375  symgcom2  33646  eulerpartlemt  35004  fineqvac  35785  subfacp1lem1  35945  cvmscld  36039  mthmpps  36348  refssfne  37147  topjoin  37154  pibt2  38342  poimirlem3  38543  poimirlem28  38568  rntrclfvOAI  43703  istopclsd  43712  nacsfix  43724  diophrw  43771  tfsconcatb0  44347  onsucunipr  44375  oaun3  44385  clcnvlem  44624  cnvrcl0  44626  dmtrcl  44628  rntrcl  44629  iunrelexp0  44703  dmtrclfvRP  44731  rntrclfv  44733  cotrclrcl  44743  clsk3nimkb  45041  limciccioolb  46634  limcicciooub  46648  ioccncflimc  46896  icocncflimc  46900  stoweidlem44  47055  dirkercncflem3  47116  fourierdlem62  47179  ismeannd  47478  cycl3grtri  49046