Theorem undif 4457

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∖ cdif 3923   ∪ cun 3924   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309

This theorem is referenced by:  undifrOLD  4459  raldifeq  4469  pwundif  4599  imadifssran  6140  fveqf1o  7294  undifixp  8946  dfdom2  8990  sbthlem5  9099  sbthlem6  9100  domunsn  9139  fodomr  9140  mapdom2  9160  limensuci  9165  findcard2  9176  ssfi  9185  fodomfir  9338  marypha1lem  9443  brwdom2  9585  infdifsn  9669  ackbij1lem12  10242  ackbij1lem18  10248  ssfin4  10322  fin23lem28  10352  fin23lem30  10354  fin1a2lem13  10424  canthp1lem1  10664  xrsupss  13323  xrinfmss  13324  hashssdif  14428  hashfun  14453  hashf1lem2  14472  fsumsplit1  15759  fsumless  15810  incexclem  15850  incexc  15851  fprodsplit1f  16004  pwssplit1  21015  frlmsslss2  21733  mdetdiaglem  22534  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  smadiadet  22606  isclo  23023  cmpcld  23338  rrxcph  25342  rrxdstprj1  25359  uniiccmbl  25541  itgss3  25766  dchreq  27219  noextendseq  27629  madeun  27839  axlowdimlem7  28873  axlowdimlem10  28876  fressupp  32611  padct  32643  resf1o  32653  fprodeq02  32748  indval2  32777  gsummptres2  32993  cycpmcl  33073  cycpmco2  33090  cyc3co2  33097  cycpmconjslem2  33112  cyc3conja  33114  elrspunidl  33389  lbsdiflsp0  33612  dimkerim  33613  locfinref  33818  esummono  34031  gsumesum  34036  sigaclfu2  34098  measxun2  34187  measvuni  34191  measssd  34192  pmeasmono  34302  eulerpartlemt  34349  tgoldbachgtde  34638  satfvsucsuc  35333  poimirlem9  37599  poimirlem15  37605  poimirlem25  37615  selvvvval  42555  evlselv  42557  fsuppssind  42563  diophrw  42729  eldioph2lem1  42730  eldioph2lem2  42731  kelac1  43034  tfsconcatfn  43309  tfsconcatrev  43319  ioccncflimc  45862  icocncflimc  45866  dirkercncflem2  46081  dirkercncflem3  46082  sge0ss  46389  meassle  46440  meadif  46456  meaiininclem  46463  isomenndlem  46507  hspmbllem1  46603  hspmbllem2  46604  ovolval4lem1  46626  fsumsplitsndif  47335  stgrclnbgr0  47925