Theorem undif 4445

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 4149	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4440	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2734	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1540   ∖ cdif 3911   ∪ cun 3912   ⊆ wss 3914

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297

This theorem is referenced by:  undifrOLD  4447  raldifeq  4457  pwundif  4587  imadifssran  6124  fveqf1o  7277  undifixp  8907  dfdom2  8949  sbthlem5  9055  sbthlem6  9056  domunsn  9091  fodomr  9092  mapdom2  9112  limensuci  9117  findcard2  9128  ssfi  9137  fodomfir  9279  marypha1lem  9384  brwdom2  9526  infdifsn  9610  ackbij1lem12  10183  ackbij1lem18  10189  ssfin4  10263  fin23lem28  10293  fin23lem30  10295  fin1a2lem13  10365  canthp1lem1  10605  xrsupss  13269  xrinfmss  13270  hashssdif  14377  hashfun  14402  hashf1lem2  14421  fsumsplit1  15711  fsumless  15762  incexclem  15802  incexc  15803  fprodsplit1f  15956  pwssplit1  20966  frlmsslss2  21684  mdetdiaglem  22485  mdetrlin  22489  mdetrsca  22490  mdetralt  22495  smadiadet  22557  isclo  22974  cmpcld  23289  rrxcph  25292  rrxdstprj1  25309  uniiccmbl  25491  itgss3  25716  dchreq  27169  noextendseq  27579  madeun  27795  axlowdimlem7  28875  axlowdimlem10  28878  fressupp  32611  padct  32643  resf1o  32653  fprodeq02  32748  indval2  32777  gsummptres2  32993  cycpmcl  33073  cycpmco2  33090  cyc3co2  33097  cycpmconjslem2  33112  cyc3conja  33114  elrspunidl  33399  lbsdiflsp0  33622  dimkerim  33623  locfinref  33831  esummono  34044  gsumesum  34049  sigaclfu2  34111  measxun2  34200  measvuni  34204  measssd  34205  pmeasmono  34315  eulerpartlemt  34362  tgoldbachgtde  34651  satfvsucsuc  35352  poimirlem9  37623  poimirlem15  37629  poimirlem25  37639  selvvvval  42573  evlselv  42575  fsuppssind  42581  diophrw  42747  eldioph2lem1  42748  eldioph2lem2  42749  kelac1  43052  tfsconcatfn  43327  tfsconcatrev  43337  ioccncflimc  45883  icocncflimc  45887  dirkercncflem2  46102  dirkercncflem3  46103  sge0ss  46410  meassle  46461  meadif  46477  meaiininclem  46484  isomenndlem  46528  hspmbllem1  46624  hspmbllem2  46625  ovolval4lem1  46647  fsumsplitsndif  47374  stgrclnbgr0  47964