Theorem undif 4049

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 3783	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4044	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2627	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 267	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 196   = wceq 1483   ∖ cdif 3571   ∪ cun 3572   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916

This theorem is referenced by:  raldifeq  4059  difsnid  4341  fveqf1o  6557  ralxpmap  7907  undifixp  7944  dfdom2  7981  sbthlem5  8074  sbthlem6  8075  domunsn  8110  fodomr  8111  mapdom2  8131  limensuci  8136  findcard2  8200  unfi  8227  marypha1lem  8339  brwdom2  8478  infdifsn  8554  ackbij1lem12  9053  ackbij1lem18  9059  ssfin4  9132  fin23lem28  9162  fin23lem30  9164  fin1a2lem13  9234  canthp1lem1  9474  xrsupss  12139  xrinfmss  12140  hashssdif  13200  hashfun  13224  hashf1lem2  13240  fsumless  14528  incexclem  14568  incexc  14569  fprodsplit1f  14721  pwssplit1  19059  frlmsslss2  20114  mdetdiaglem  20404  mdetrlin  20408  mdetrsca  20409  mdetralt  20414  smadiadet  20476  isclo  20891  cmpcld  21205  rrxcph  23180  rrxdstprj1  23192  uniiccmbl  23358  itgss3  23581  dchreq  24983  axlowdimlem7  25828  axlowdimlem10  25831  padct  29497  resf1o  29505  fprodeq02  29569  locfinref  29908  indval2  30076  esummono  30116  gsumesum  30121  sigaclfu2  30184  measxun2  30273  measvuni  30277  measssd  30278  pmeasmono  30386  eulerpartlemt  30433  tgoldbachgtde  30738  noextendseq  31820  poimirlem9  33418  poimirlem15  33424  poimirlem25  33434  diophrw  37322  eldioph2lem1  37323  eldioph2lem2  37324  kelac1  37633  fsumsplit1  39804  ioccncflimc  40098  icocncflimc  40102  dirkercncflem2  40321  dirkercncflem3  40322  sge0ss  40629  meassle  40680  meadif  40696  meaiininclem  40700  isomenndlem  40744  hspmbllem1  40840  hspmbllem2  40841  ovolval4lem1  40863  fsumsplitsndif  41343