Theorem undif 4441

Description: Union of complementary parts into whole. (Contributed by NM, 22-Mar-1998.)

Assertion

Ref	Expression
undif	⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Proof of Theorem undif

Step	Hyp	Ref	Expression
1		ssequn1 4135	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4434	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2767	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∖ cdif 3899   ∪ cun 3900   ⊆ wss 3902

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 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283

This theorem is used by:  raldifeq  4452  pwundif  4585  imadifssranOLD  6202  fveqf1o  7307  undifixp  8945  dfdom2  8988  sbthlem5  9093  sbthlem6  9094  domunsn  9129  fodomr  9130  mapdom2  9150  limensuci  9155  findcard2  9163  ssfi  9171  fodomfir  9301  marypha1lem  9407  brwdom2  9549  infdifsn  9640  ackbij1lem12  10236  ackbij1lem18  10242  ssfin4  10316  fin23lem28  10346  fin23lem30  10348  fin1a2lem13  10418  canthp1lem1  10665  indval2  12251  xrsupss  13365  xrinfmss  13366  hashssdif  14481  hashfun  14506  hashf1lem2  14525  fsumsplit1  15835  fsumless  15887  incexclem  15929  incexc  15930  fprodsplit1f  16083  pwssplit1  21249  frlmsslss2  21994  selvvvval  22364  mdetdiaglem  22826  mdetrlin  22830  mdetrsca  22831  mdetralt  22836  smadiadet  22898  isclo  23318  cmpcld  23633  rrxcph  25626  rrxdstprj1  25643  uniiccmbl  25824  itgss3  26049  dchreq  27502  noextendseq  27911  madeun  28157  axlowdimlem7  29413  axlowdimlem10  29416  fressupp  33168  padct  33197  resf1o  33209  fprodeq02  33302  gsummptres2  33501  cycpmcl  33564  cycpmco2  33581  cyc3co2  33588  cycpmconjslem2  33603  cyc3conja  33605  elrspunidl  33864  lbsdiflsp0  34144  dimkerim  34145  locfinref  34359  esummono  34572  gsumesum  34577  sigaclfu2  34639  measxun2  34729  measvuni  34733  measssd  34734  pmeasmono  34843  eulerpartlemt  34890  tgoldbachgtde  35176  satfvsucsuc  35952  poimirlem9  38386  poimirlem15  38392  poimirlem25  38402  evlselv  43443  fsuppssind  43447  diophrw  43612  eldioph2lem1  43613  eldioph2lem2  43614  kelac1  43912  tfsconcatfn  44187  tfsconcatrev  44197  ioccncflimc  46721  icocncflimc  46725  dirkercncflem2  46940  dirkercncflem3  46941  sge0ss  47248  meassle  47299  meadif  47315  meaiininclem  47322  isomenndlem  47366  hspmbllem1  47462  hspmbllem2  47463  ovolval4lem1  47485  fsumsplitsndif  48277  stgrclnbgr0  48889