Theorem undif 4417

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 4122	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4412	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2745	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 279	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 207   = wceq 1547   ∖ 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 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269

This theorem is referenced by:  raldifeq  4428  pwundif  4560  imadifssran  6109  fveqf1o  7253  undifixp  8879  dfdom2  8922  sbthlem5  9026  sbthlem6  9027  domunsn  9062  fodomr  9063  mapdom2  9083  limensuci  9088  findcard2  9096  ssfi  9104  fodomfir  9235  marypha1lem  9343  brwdom2  9485  infdifsn  9576  ackbij1lem12  10150  ackbij1lem18  10156  ssfin4  10230  fin23lem28  10260  fin23lem30  10262  fin1a2lem13  10332  canthp1lem1  10573  indval2  12162  xrsupss  13259  xrinfmss  13260  hashssdif  14372  hashfun  14397  hashf1lem2  14416  fsumsplit1  15705  fsumless  15757  incexclem  15799  incexc  15800  fprodsplit1f  15953  pwssplit1  21056  frlmsslss2  21757  selvvvval  22125  mdetdiaglem  22588  mdetrlin  22592  mdetrsca  22593  mdetralt  22598  smadiadet  22660  isclo  23077  cmpcld  23392  rrxcph  25384  rrxdstprj1  25401  uniiccmbl  25582  itgss3  25807  dchreq  27246  noextendseq  27656  madeun  27901  axlowdimlem7  29042  axlowdimlem10  29045  fressupp  32787  padct  32817  resf1o  32829  fprodeq02  32923  gsummptres2  33141  cycpmcl  33204  cycpmco2  33221  cyc3co2  33228  cycpmconjslem2  33243  cyc3conja  33245  elrspunidl  33518  lbsdiflsp0  33817  dimkerim  33818  locfinref  34032  esummono  34245  gsumesum  34250  sigaclfu2  34312  measxun2  34401  measvuni  34405  measssd  34406  pmeasmono  34515  eulerpartlemt  34562  tgoldbachgtde  34851  satfvsucsuc  35600  poimirlem9  38003  poimirlem15  38009  poimirlem25  38019  evlselv  43046  fsuppssind  43050  diophrw  43215  eldioph2lem1  43216  eldioph2lem2  43217  kelac1  43515  tfsconcatfn  43790  tfsconcatrev  43800  ioccncflimc  46335  icocncflimc  46339  dirkercncflem2  46554  dirkercncflem3  46555  sge0ss  46862  meassle  46913  meadif  46929  meaiininclem  46936  isomenndlem  46980  hspmbllem1  47076  hspmbllem2  47077  ovolval4lem1  47099  fsumsplitsndif  47851  stgrclnbgr0  48463