Theorem undif 4441

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 4187	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4434	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2768	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3900   ∖ cdif 4048   ∪ cun 4152

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282

This theorem is used by:  raldifeq  4452  pwundif  4586  imadifssranOLDOLD  6216  fveqf1o  7333  undifixp  8990  dfdom2  9033  sbthlem5  9138  sbthlem6  9139  domunsn  9174  fodomr  9175  mapdom2  9195  limensuci  9200  findcard2  9208  ssfi  9216  fodomfir  9347  marypha1lem  9452  brwdom2  9594  infdifsn  9685  ackbij1lem12  10335  ackbij1lem18  10341  ssfin4  10415  fin23lem28  10445  fin23lem30  10447  fin1a2lem13  10517  canthp1lem1  10764  indval2  12352  xrsupss  13466  xrinfmss  13467  hashssdif  14584  hashfun  14609  hashf1lem2  14628  fsumsplit1  15940  fsumless  15992  incexclem  16034  incexc  16035  fprodsplit1f  16186  pwssplit1  21364  frlmsslss2  22111  selvvvval  22481  mdetdiaglem  22943  mdetrlin  22947  mdetrsca  22948  mdetralt  22953  smadiadet  23015  isclo  23435  cmpcld  23750  rrxcph  25743  rrxdstprj1  25760  uniiccmbl  25941  itgss3  26165  dchreq  27615  noextendseq  28054  madeun  28300  axlowdimlem7  29556  axlowdimlem10  29559  fressupp  33352  padct  33381  resf1o  33392  fprodeq02  33485  gsummptres2  33684  cycpmcl  33747  cycpmco2  33764  cyc3co2  33771  cycpmconjslem2  33786  cyc3conja  33788  elrspunidl  34048  lbsdiflsp0  34328  dimkerim  34329  locfinref  34543  esummono  34756  gsumesum  34761  sigaclfu2  34823  measxun2  34913  measvuni  34917  measssd  34918  pmeasmono  35026  eulerpartlemt  35073  tgoldbachgtde  35359  satfvsucsuc  36297  poimirlem9  38739  poimirlem15  38745  poimirlem25  38755  evlselv  43810  fsuppssind  43814  diophrw  43963  eldioph2lem1  43964  eldioph2lem2  43965  kelac1  44258  tfsconcatfn  44532  tfsconcatrev  44542  ioccncflimc  47100  icocncflimc  47104  dirkercncflem2  47319  dirkercncflem3  47320  sge0ss  47627  meassle  47678  meadif  47694  meaiininclem  47701  isomenndlem  47745  hspmbllem1  47841  hspmbllem2  47842  ovolval4lem1  47864  fsumsplitsndif  48656  stgrclnbgr0  49268