Theorem undif 4435

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 4138	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4430	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2766	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 280	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 208   = wceq 1559   ∖ cdif 3901   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286

This theorem is referenced by:  raldifeq  4446  pwundif  4579  imadifssran  6133  fveqf1o  7282  undifixp  8912  dfdom2  8955  sbthlem5  9059  sbthlem6  9060  domunsn  9095  fodomr  9096  mapdom2  9116  limensuci  9121  findcard2  9129  ssfi  9137  fodomfir  9268  marypha1lem  9376  brwdom2  9518  infdifsn  9609  ackbij1lem12  10183  ackbij1lem18  10189  ssfin4  10264  fin23lem28  10294  fin23lem30  10296  fin1a2lem13  10366  canthp1lem1  10607  indval2  12197  xrsupss  13309  xrinfmss  13310  hashssdif  14422  hashfun  14447  hashf1lem2  14466  fsumsplit1  15755  fsumless  15807  incexclem  15849  incexc  15850  fprodsplit1f  16003  pwssplit1  21106  frlmsslss2  21807  selvvvval  22175  mdetdiaglem  22638  mdetrlin  22642  mdetrsca  22643  mdetralt  22648  smadiadet  22710  isclo  23127  cmpcld  23442  rrxcph  25434  rrxdstprj1  25451  uniiccmbl  25632  itgss3  25857  dchreq  27299  noextendseq  27708  madeun  27954  axlowdimlem7  29095  axlowdimlem10  29098  fressupp  32840  padct  32870  resf1o  32882  fprodeq02  32976  gsummptres2  33194  cycpmcl  33257  cycpmco2  33274  cyc3co2  33281  cycpmconjslem2  33296  cyc3conja  33298  elrspunidl  33575  lbsdiflsp0  33884  dimkerim  33885  locfinref  34099  esummono  34312  gsumesum  34317  sigaclfu2  34379  measxun2  34468  measvuni  34472  measssd  34473  pmeasmono  34582  eulerpartlemt  34629  tgoldbachgtde  34918  satfvsucsuc  35679  poimirlem9  38092  poimirlem15  38098  poimirlem25  38108  evlselv  43135  fsuppssind  43139  diophrw  43304  eldioph2lem1  43305  eldioph2lem2  43306  kelac1  43604  tfsconcatfn  43879  tfsconcatrev  43889  ioccncflimc  46423  icocncflimc  46427  dirkercncflem2  46642  dirkercncflem3  46643  sge0ss  46950  meassle  47001  meadif  47017  meaiininclem  47024  isomenndlem  47068  hspmbllem1  47164  hspmbllem2  47165  ovolval4lem1  47187  fsumsplitsndif  47939  stgrclnbgr0  48551