Theorem ssequn2 4145

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

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

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-ss 3925

This theorem is used by:  unabs  4221  undifr  4449  tppreqb  4778  pwssun  5558  cnvimassrndm  6154  relresfldOLD  6284  ordssun  6472  ordequn  6473  onunel  6475  onun2  6478  oneluni  6488  fsnunf  7190  sorpssun  7740  ordunpr  7831  omun  7893  fodomr  9126  unfi  9165  enp1ilem  9248  pwfilem  9287  fodomfir  9297  brwdom2  9545  sucprcreg  9578  sucprcregOLD  9579  dfacfin7  10401  hashbclem  14509  incexclem  15916  ramub1lem1  17111  ramub1lem2  17112  mreexmrid  17724  lspun0  21169  lbsextlem4  21322  cldlp  23344  ordtuni  23384  lfinun  23719  cldsubg  24305  trust  24423  nulmbl2  25732  limcmpt2  26080  cnplimc  26083  dvreslem  26105  dvaddbr  26134  dvmulbr  26135  lhop  26212  plypf1  26406  coeeulem  26418  coeeu  26419  coef2  26425  rlimcnp  27167  noetalem1  27942  addsproplem2  28200  ex-un  30812  shs0i  31838  chj0i  31844  disjun0  32977  ffsrn  33110  difioo  33164  symgcom2  33435  eulerpartlemt  34792  fineqvac  35552  subfacp1lem1  35691  cvmscld  35785  mthmpps  36094  refssfne  36909  topjoin  36916  pibt2  38103  poimirlem3  38314  poimirlem28  38339  rntrclfvOAI  43462  istopclsd  43471  nacsfix  43483  diophrw  43530  tfsconcatb0  44111  onsucunipr  44139  oaun3  44149  clcnvlem  44389  cnvrcl0  44391  dmtrcl  44393  rntrcl  44394  iunrelexp0  44468  dmtrclfvRP  44496  rntrclfv  44498  cotrclrcl  44508  clsk3nimkb  44806  limciccioolb  46377  limcicciooub  46391  ioccncflimc  46639  icocncflimc  46643  stoweidlem44  46798  dirkercncflem3  46859  fourierdlem62  46922  ismeannd  47221  cycl3grtri  48752