Theorem ssequn2 4155

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3915   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934

This theorem is referenced by:  unabs  4231  undifr  4449  tppreqb  4772  pwssun  5533  cnvimassrndm  6128  relresfld  6252  ordssun  6439  ordequn  6440  onunel  6442  onun2  6445  oneluni  6456  fsnunf  7162  sorpssun  7709  ordunpr  7804  omun  7867  fodomr  9098  unfi  9141  enp1ilem  9230  pwfilem  9274  fodomfir  9286  brwdom2  9533  sucprcreg  9561  dfacfin7  10359  hashbclem  14424  incexclem  15809  ramub1lem1  17004  ramub1lem2  17005  mreexmrid  17611  lspun0  20924  lbsextlem4  21078  cldlp  23044  ordtuni  23084  lfinun  23419  cldsubg  24005  trust  24124  nulmbl2  25444  limcmpt2  25792  cnplimc  25795  dvreslem  25817  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  lhop  25928  plypf1  26124  coeeulem  26136  coeeu  26137  coef2  26143  rlimcnp  26882  noetalem1  27660  addsproplem2  27884  ex-un  30360  shs0i  31385  chj0i  31391  disjun0  32531  ffsrn  32659  difioo  32712  symgcom2  33048  eulerpartlemt  34369  fineqvac  35094  subfacp1lem1  35173  cvmscld  35267  mthmpps  35576  refssfne  36353  topjoin  36360  pibt2  37412  poimirlem3  37624  poimirlem28  37649  rntrclfvOAI  42686  istopclsd  42695  nacsfix  42707  diophrw  42754  tfsconcatb0  43340  onsucunipr  43368  oaun3  43378  clcnvlem  43619  cnvrcl0  43621  dmtrcl  43623  rntrcl  43624  iunrelexp0  43698  dmtrclfvRP  43726  rntrclfv  43728  cotrclrcl  43738  clsk3nimkb  44036  limciccioolb  45626  limcicciooub  45642  ioccncflimc  45890  icocncflimc  45894  stoweidlem44  46049  dirkercncflem3  46110  fourierdlem62  46173  ismeannd  46472  cycl3grtri  47950