Theorem undif 4338

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 4072	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4333	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2798	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 279	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 207   = wceq 1520   ∖ cdif 3851   ∪ cun 3852   ⊆ wss 3854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207

This theorem is referenced by:  raldifeq  4347  difsnid  4644  fveqf1o  6914  ralxpmap  8299  undifixp  8336  dfdom2  8373  sbthlem5  8468  sbthlem6  8469  domunsn  8504  fodomr  8505  mapdom2  8525  limensuci  8530  findcard2  8594  unfi  8621  marypha1lem  8733  brwdom2  8873  infdifsn  8955  ackbij1lem12  9488  ackbij1lem18  9494  ssfin4  9567  fin23lem28  9597  fin23lem30  9599  fin1a2lem13  9669  canthp1lem1  9909  xrsupss  12541  xrinfmss  12542  hashssdif  13609  hashfun  13634  hashf1lem2  13650  fsumless  14972  incexclem  15012  incexc  15013  fprodsplit1f  15165  pwssplit1  19509  frlmsslss2  20589  mdetdiaglem  20879  mdetrlin  20883  mdetrsca  20884  mdetralt  20889  smadiadet  20951  isclo  21367  cmpcld  21682  rrxcph  23666  rrxdstprj1  23683  uniiccmbl  23862  itgss3  24086  dchreq  25504  axlowdimlem7  26405  axlowdimlem10  26408  padct  30116  resf1o  30127  fprodeq02  30194  cycpmcl  30369  cyc3co2  30382  cycpmconjslem2  30393  cyc3conja  30395  lbsdiflsp0  30581  dimkerim  30582  locfinref  30678  indval2  30846  esummono  30886  gsumesum  30891  sigaclfu2  30953  measxun2  31042  measvuni  31046  measssd  31047  pmeasmono  31155  eulerpartlemt  31202  tgoldbachgtde  31504  satfvsucsuc  32174  noextendseq  32728  poimirlem9  34378  poimirlem15  34384  poimirlem25  34394  diophrw  38791  eldioph2lem1  38792  eldioph2lem2  38793  kelac1  39099  fsumsplit1  41349  ioccncflimc  41663  icocncflimc  41667  dirkercncflem2  41885  dirkercncflem3  41886  sge0ss  42190  meassle  42241  meadif  42257  meaiininclem  42264  isomenndlem  42308  hspmbllem1  42404  hspmbllem2  42405  ovolval4lem1  42427  fsumsplitsndif  43003