Theorem ssequn2 4143

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∪ cun 3901   ⊆ wss 3903

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 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  unabs  4219  undifr  4437  tppreqb  4763  pwssun  5524  cnvimassrndm  6118  relresfld  6242  ordssun  6429  ordequn  6430  onunel  6432  onun2  6435  oneluni  6445  fsnunf  7141  sorpssun  7685  ordunpr  7778  omun  7840  fodomr  9068  unfi  9107  enp1ilem  9190  pwfilem  9230  fodomfir  9240  brwdom2  9490  sucprcreg  9521  dfacfin7  10321  hashbclem  14387  incexclem  15771  ramub1lem1  16966  ramub1lem2  16967  mreexmrid  17578  lspun0  20974  lbsextlem4  21128  cldlp  23106  ordtuni  23146  lfinun  23481  cldsubg  24067  trust  24185  nulmbl2  25505  limcmpt2  25853  cnplimc  25856  dvreslem  25878  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  lhop  25989  plypf1  26185  coeeulem  26197  coeeu  26198  coef2  26204  rlimcnp  26943  noetalem1  27721  addsproplem2  27978  ex-un  30511  shs0i  31536  chj0i  31542  disjun0  32681  ffsrn  32817  difioo  32872  symgcom2  33177  eulerpartlemt  34548  fineqvac  35291  subfacp1lem1  35392  cvmscld  35486  mthmpps  35795  refssfne  36571  topjoin  36578  pibt2  37666  poimirlem3  37868  poimirlem28  37893  rntrclfvOAI  43042  istopclsd  43051  nacsfix  43063  diophrw  43110  tfsconcatb0  43695  onsucunipr  43723  oaun3  43733  clcnvlem  43973  cnvrcl0  43975  dmtrcl  43977  rntrcl  43978  iunrelexp0  44052  dmtrclfvRP  44080  rntrclfv  44082  cotrclrcl  44092  clsk3nimkb  44390  limciccioolb  45975  limcicciooub  45989  ioccncflimc  46237  icocncflimc  46241  stoweidlem44  46396  dirkercncflem3  46457  fourierdlem62  46520  ismeannd  46819  cycl3grtri  48301