Theorem undif 4432

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 4158	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4427	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2828	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 280	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1537   ∖ cdif 3935   ∪ cun 3936   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294

This theorem is referenced by:  raldifeq  4441  pwundif  4567  difsnid  4745  fveqf1o  7060  ralxpmap  8462  undifixp  8500  dfdom2  8537  sbthlem5  8633  sbthlem6  8634  domunsn  8669  fodomr  8670  mapdom2  8690  limensuci  8695  findcard2  8760  unfi  8787  marypha1lem  8899  brwdom2  9039  infdifsn  9122  ackbij1lem12  9655  ackbij1lem18  9661  ssfin4  9734  fin23lem28  9764  fin23lem30  9766  fin1a2lem13  9836  canthp1lem1  10076  xrsupss  12705  xrinfmss  12706  hashssdif  13776  hashfun  13801  hashf1lem2  13817  fsumless  15153  incexclem  15193  incexc  15194  fprodsplit1f  15346  pwssplit1  19833  frlmsslss2  20921  mdetdiaglem  21209  mdetrlin  21213  mdetrsca  21214  mdetralt  21219  smadiadet  21281  isclo  21697  cmpcld  22012  rrxcph  23997  rrxdstprj1  24014  uniiccmbl  24193  itgss3  24417  dchreq  25836  axlowdimlem7  26736  axlowdimlem10  26739  undifr  30286  padct  30457  resf1o  30468  fprodeq02  30541  cycpmcl  30760  cycpmco2  30777  cyc3co2  30784  cycpmconjslem2  30799  cyc3conja  30801  lbsdiflsp0  31024  dimkerim  31025  locfinref  31107  indval2  31275  esummono  31315  gsumesum  31320  sigaclfu2  31382  measxun2  31471  measvuni  31475  measssd  31476  pmeasmono  31584  eulerpartlemt  31631  tgoldbachgtde  31933  satfvsucsuc  32614  noextendseq  33176  poimirlem9  34903  poimirlem15  34909  poimirlem25  34919  diophrw  39363  eldioph2lem1  39364  eldioph2lem2  39365  kelac1  39670  fsumsplit1  41860  ioccncflimc  42175  icocncflimc  42179  dirkercncflem2  42396  dirkercncflem3  42397  sge0ss  42701  meassle  42752  meadif  42768  meaiininclem  42775  isomenndlem  42819  hspmbllem1  42915  hspmbllem2  42916  ovolval4lem1  42938  fsumsplitsndif  43540