Theorem ssequn2 4130

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 4127	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		uncom 4099	. . 3 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2742	. 2 ⊢ ((𝐴 ∪ 𝐵) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitri 275	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ∪ cun 3888   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  unabs  4206  undifr  4424  tppreqb  4749  pwssun  5516  cnvimassrndm  6110  relresfld  6234  ordssun  6421  ordequn  6422  onunel  6424  onun2  6427  oneluni  6437  fsnunf  7133  sorpssun  7677  ordunpr  7770  omun  7832  fodomr  9059  unfi  9098  enp1ilem  9181  pwfilem  9221  fodomfir  9231  brwdom2  9481  sucprcreg  9512  dfacfin7  10312  hashbclem  14405  incexclem  15792  ramub1lem1  16988  ramub1lem2  16989  mreexmrid  17600  lspun0  20997  lbsextlem4  21151  cldlp  23125  ordtuni  23165  lfinun  23500  cldsubg  24086  trust  24204  nulmbl2  25513  limcmpt2  25861  cnplimc  25864  dvreslem  25886  dvaddbr  25915  dvmulbr  25916  lhop  25993  plypf1  26187  coeeulem  26199  coeeu  26200  coef2  26206  rlimcnp  26942  noetalem1  27719  addsproplem2  27976  ex-un  30509  shs0i  31535  chj0i  31541  disjun0  32680  ffsrn  32816  difioo  32870  symgcom2  33160  eulerpartlemt  34531  fineqvac  35276  subfacp1lem1  35377  cvmscld  35471  mthmpps  35780  refssfne  36556  topjoin  36563  pibt2  37747  poimirlem3  37958  poimirlem28  37983  rntrclfvOAI  43137  istopclsd  43146  nacsfix  43158  diophrw  43205  tfsconcatb0  43790  onsucunipr  43818  oaun3  43828  clcnvlem  44068  cnvrcl0  44070  dmtrcl  44072  rntrcl  44073  iunrelexp0  44147  dmtrclfvRP  44175  rntrclfv  44177  cotrclrcl  44187  clsk3nimkb  44485  limciccioolb  46069  limcicciooub  46083  ioccncflimc  46331  icocncflimc  46335  stoweidlem44  46490  dirkercncflem3  46551  fourierdlem62  46614  ismeannd  46913  cycl3grtri  48435