Theorem undif 4444

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 4140	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4439	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2768	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1570   ∖ cdif 3903   ∪ cun 3904   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288

This theorem is referenced by:  raldifeq  4455  pwundif  4588  imadifssranOLD  6205  fveqf1o  7302  undifixp  8933  dfdom2  8976  sbthlem5  9080  sbthlem6  9081  domunsn  9116  fodomr  9117  mapdom2  9137  limensuci  9142  findcard2  9150  ssfi  9158  fodomfir  9288  marypha1lem  9394  brwdom2  9536  infdifsn  9627  ackbij1lem12  10214  ackbij1lem18  10220  ssfin4  10295  fin23lem28  10325  fin23lem30  10327  fin1a2lem13  10397  canthp1lem1  10638  indval2  12224  xrsupss  13336  xrinfmss  13337  hashssdif  14451  hashfun  14476  hashf1lem2  14495  fsumsplit1  15798  fsumless  15850  incexclem  15892  incexc  15893  fprodsplit1f  16046  pwssplit1  21161  frlmsslss2  21906  selvvvval  22274  mdetdiaglem  22736  mdetrlin  22740  mdetrsca  22741  mdetralt  22746  smadiadet  22808  isclo  23225  cmpcld  23540  rrxcph  25532  rrxdstprj1  25549  uniiccmbl  25730  itgss3  25955  dchreq  27400  noextendseq  27809  madeun  28055  axlowdimlem7  29276  axlowdimlem10  29279  fressupp  33011  padct  33041  resf1o  33053  fprodeq02  33146  gsummptres2  33351  cycpmcl  33414  cycpmco2  33431  cyc3co2  33438  cycpmconjslem2  33453  cyc3conja  33455  elrspunidl  33714  lbsdiflsp0  33994  dimkerim  33995  locfinref  34209  esummono  34422  gsumesum  34427  sigaclfu2  34489  measxun2  34578  measvuni  34582  measssd  34583  pmeasmono  34692  eulerpartlemt  34739  tgoldbachgtde  35025  satfvsucsuc  35835  poimirlem9  38258  poimirlem15  38264  poimirlem25  38274  evlselv  43301  fsuppssind  43305  diophrw  43470  eldioph2lem1  43471  eldioph2lem2  43472  kelac1  43770  tfsconcatfn  44045  tfsconcatrev  44055  ioccncflimc  46579  icocncflimc  46583  dirkercncflem2  46798  dirkercncflem3  46799  sge0ss  47106  meassle  47157  meadif  47173  meaiininclem  47180  isomenndlem  47224  hspmbllem1  47320  hspmbllem2  47321  ovolval4lem1  47343  fsumsplitsndif  48095  stgrclnbgr0  48707