Theorem ssequn2 4183

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∪ cun 3946   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  unabs  4254  undifr  4482  tppreqb  4808  pwssun  5571  cnvimassrndm  6149  relresfld  6273  ordssun  6464  ordequn  6465  onunel  6467  onun2  6470  oneluni  6481  fsnunf  7180  sorpssun  7717  ordunpr  7811  omun  7875  fodomr  9125  unfi  9169  pwfilem  9174  enp1ilem  9275  pwfilemOLD  9343  brwdom2  9565  sucprcreg  9593  dfacfin7  10391  hashbclem  14408  incexclem  15779  ramub1lem1  16956  ramub1lem2  16957  mreexmrid  17584  lspun0  20615  lbsextlem4  20767  cldlp  22646  ordtuni  22686  lfinun  23021  cldsubg  23607  trust  23726  nulmbl2  25045  limcmpt2  25393  cnplimc  25396  dvreslem  25418  dvaddbr  25447  dvmulbr  25448  lhop  25525  plypf1  25718  coeeulem  25730  coeeu  25731  coef2  25737  rlimcnp  26460  noetalem1  27234  addsproplem2  27444  ex-un  29667  shs0i  30690  chj0i  30696  disjun0  31814  ffsrn  31942  difioo  31981  symgcom2  32233  eulerpartlemt  33359  fineqvac  34086  subfacp1lem1  34159  cvmscld  34253  mthmpps  34562  gg-dvmulbr  35164  refssfne  35232  topjoin  35239  pibt2  36287  poimirlem3  36480  poimirlem28  36505  rntrclfvOAI  41415  istopclsd  41424  nacsfix  41436  diophrw  41483  tfsconcatb0  42080  onsucunipr  42108  oaun3  42118  clcnvlem  42360  cnvrcl0  42362  dmtrcl  42364  rntrcl  42365  iunrelexp0  42439  dmtrclfvRP  42467  rntrclfv  42469  cotrclrcl  42479  clsk3nimkb  42777  limciccioolb  44324  limcicciooub  44340  ioccncflimc  44588  icocncflimc  44592  stoweidlem44  44747  dirkercncflem3  44808  fourierdlem62  44871  ismeannd  45170