Theorem undif 4477

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

Syntax hints:   ↔ wb 205   = wceq 1534   ∖ cdif 3941   ∪ cun 3942   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319

This theorem is referenced by:  undifrOLD  4479  raldifeq  4489  pwundif  4622  fveqf1o  7306  undifixp  8944  dfdom2  8990  sbthlem5  9103  sbthlem6  9104  domunsn  9143  fodomr  9144  mapdom2  9164  limensuci  9169  findcard2  9180  ssfi  9189  findcard2OLD  9300  unfiOLD  9329  marypha1lem  9448  brwdom2  9588  infdifsn  9672  ackbij1lem12  10246  ackbij1lem18  10252  ssfin4  10325  fin23lem28  10355  fin23lem30  10357  fin1a2lem13  10427  canthp1lem1  10667  xrsupss  13312  xrinfmss  13313  hashssdif  14395  hashfun  14420  hashf1lem2  14441  fsumsplit1  15715  fsumless  15766  incexclem  15806  incexc  15807  fprodsplit1f  15958  pwssplit1  20933  frlmsslss2  21696  mdetdiaglem  22487  mdetrlin  22491  mdetrsca  22492  mdetralt  22497  smadiadet  22559  isclo  22978  cmpcld  23293  rrxcph  25307  rrxdstprj1  25324  uniiccmbl  25506  itgss3  25731  dchreq  27178  noextendseq  27587  madeun  27797  axlowdimlem7  28746  axlowdimlem10  28749  fressupp  32452  padct  32485  resf1o  32496  fprodeq02  32568  gsummptres2  32745  cycpmcl  32815  cycpmco2  32832  cyc3co2  32839  cycpmconjslem2  32854  cyc3conja  32856  elrspunidl  33079  lbsdiflsp0  33256  dimkerim  33257  locfinref  33378  indval2  33569  esummono  33609  gsumesum  33614  sigaclfu2  33676  measxun2  33765  measvuni  33769  measssd  33770  pmeasmono  33880  eulerpartlemt  33927  tgoldbachgtde  34228  satfvsucsuc  34911  poimirlem9  37037  poimirlem15  37043  poimirlem25  37053  selvvvval  41740  evlselv  41742  fsuppssind  41748  diophrw  42101  eldioph2lem1  42102  eldioph2lem2  42103  kelac1  42409  tfsconcatfn  42690  tfsconcatrev  42700  ioccncflimc  45196  icocncflimc  45200  dirkercncflem2  45415  dirkercncflem3  45416  sge0ss  45723  meassle  45774  meadif  45790  meaiininclem  45797  isomenndlem  45841  hspmbllem1  45937  hspmbllem2  45938  ovolval4lem1  45960  fsumsplitsndif  46636