Theorem undif 4448

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∖ cdif 3905   ∪ cun 3906   ⊆ wss 3908

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

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 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290

This theorem is used by:  raldifeq  4459  pwundif  4592  imadifssranOLD  6208  fveqf1o  7311  undifixp  8941  dfdom2  8984  sbthlem5  9089  sbthlem6  9090  domunsn  9125  fodomr  9126  mapdom2  9146  limensuci  9151  findcard2  9159  ssfi  9167  fodomfir  9297  marypha1lem  9403  brwdom2  9545  infdifsn  9636  ackbij1lem12  10232  ackbij1lem18  10238  ssfin4  10312  fin23lem28  10342  fin23lem30  10344  fin1a2lem13  10414  canthp1lem1  10655  indval2  12241  xrsupss  13353  xrinfmss  13354  hashssdif  14469  hashfun  14494  hashf1lem2  14513  fsumsplit1  15822  fsumless  15874  incexclem  15916  incexc  15917  fprodsplit1f  16070  pwssplit1  21217  frlmsslss2  21962  selvvvval  22330  mdetdiaglem  22792  mdetrlin  22796  mdetrsca  22797  mdetralt  22802  smadiadet  22864  isclo  23281  cmpcld  23596  rrxcph  25588  rrxdstprj1  25605  uniiccmbl  25786  itgss3  26011  dchreq  27459  noextendseq  27868  madeun  28114  axlowdimlem7  29335  axlowdimlem10  29338  fressupp  33070  padct  33100  resf1o  33112  fprodeq02  33205  gsummptres2  33404  cycpmcl  33467  cycpmco2  33484  cyc3co2  33491  cycpmconjslem2  33506  cyc3conja  33508  elrspunidl  33767  lbsdiflsp0  34047  dimkerim  34048  locfinref  34262  esummono  34475  gsumesum  34480  sigaclfu2  34542  measxun2  34632  measvuni  34636  measssd  34637  pmeasmono  34746  eulerpartlemt  34793  tgoldbachgtde  35079  satfvsucsuc  35878  poimirlem9  38321  poimirlem15  38327  poimirlem25  38337  evlselv  43362  fsuppssind  43366  diophrw  43531  eldioph2lem1  43532  eldioph2lem2  43533  kelac1  43831  tfsconcatfn  44106  tfsconcatrev  44116  ioccncflimc  46640  icocncflimc  46644  dirkercncflem2  46859  dirkercncflem3  46860  sge0ss  47167  meassle  47218  meadif  47234  meaiininclem  47241  isomenndlem  47285  hspmbllem1  47381  hspmbllem2  47382  ovolval4lem1  47404  fsumsplitsndif  48159  stgrclnbgr0  48771