Theorem undif 4423

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∖ cdif 3887   ∪ cun 3888   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275

This theorem is referenced by:  raldifeq  4434  pwundif  4566  imadifssran  6109  fveqf1o  7250  undifixp  8875  dfdom2  8918  sbthlem5  9022  sbthlem6  9023  domunsn  9058  fodomr  9059  mapdom2  9079  limensuci  9084  findcard2  9092  ssfi  9100  fodomfir  9231  marypha1lem  9339  brwdom2  9481  infdifsn  9569  ackbij1lem12  10143  ackbij1lem18  10149  ssfin4  10223  fin23lem28  10253  fin23lem30  10255  fin1a2lem13  10325  canthp1lem1  10566  indval2  12155  xrsupss  13252  xrinfmss  13253  hashssdif  14365  hashfun  14390  hashf1lem2  14409  fsumsplit1  15698  fsumless  15750  incexclem  15792  incexc  15793  fprodsplit1f  15946  pwssplit1  21046  frlmsslss2  21765  mdetdiaglem  22573  mdetrlin  22577  mdetrsca  22578  mdetralt  22583  smadiadet  22645  isclo  23062  cmpcld  23377  rrxcph  25369  rrxdstprj1  25386  uniiccmbl  25567  itgss3  25792  dchreq  27235  noextendseq  27645  madeun  27890  axlowdimlem7  29031  axlowdimlem10  29034  fressupp  32776  padct  32806  resf1o  32818  fprodeq02  32912  gsummptres2  33129  cycpmcl  33192  cycpmco2  33209  cyc3co2  33216  cycpmconjslem2  33231  cyc3conja  33233  elrspunidl  33503  lbsdiflsp0  33786  dimkerim  33787  locfinref  34001  esummono  34214  gsumesum  34219  sigaclfu2  34281  measxun2  34370  measvuni  34374  measssd  34375  pmeasmono  34484  eulerpartlemt  34531  tgoldbachgtde  34820  satfvsucsuc  35563  poimirlem9  37964  poimirlem15  37970  poimirlem25  37980  selvvvval  43032  evlselv  43034  fsuppssind  43040  diophrw  43205  eldioph2lem1  43206  eldioph2lem2  43207  kelac1  43509  tfsconcatfn  43784  tfsconcatrev  43794  ioccncflimc  46331  icocncflimc  46335  dirkercncflem2  46550  dirkercncflem3  46551  sge0ss  46858  meassle  46909  meadif  46925  meaiininclem  46932  isomenndlem  46976  hspmbllem1  47072  hspmbllem2  47073  ovolval4lem1  47095  fsumsplitsndif  47841  stgrclnbgr0  48453