Theorem undif 4000

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 3744	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 3995	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2614	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 265	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 194   = wceq 1474   ∖ cdif 3536   ∪ cun 3537   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874

This theorem is referenced by:  raldifeq  4010  difsnid  4281  fveqf1o  6435  ralxpmap  7770  undifixp  7807  dfdom2  7844  sbthlem5  7936  sbthlem6  7937  domunsn  7972  fodomr  7973  mapdom2  7993  limensuci  7998  findcard2  8062  unfi  8089  marypha1lem  8199  brwdom2  8338  infdifsn  8414  ackbij1lem12  8913  ackbij1lem18  8919  ssfin4  8992  fin23lem28  9022  fin23lem30  9024  fin1a2lem13  9094  canthp1lem1  9330  xrsupss  11967  xrinfmss  11968  hashssdif  13013  hashfun  13036  hashf1lem2  13049  fsumless  14315  incexclem  14353  incexc  14354  fprodsplit1f  14506  pwssplit1  18826  frlmsslss2  19875  mdetdiaglem  20165  mdetrlin  20169  mdetrsca  20170  mdetralt  20175  smadiadet  20237  isclo  20643  cmpcld  20957  rrxcph  22905  rrxdstprj1  22917  uniiccmbl  23081  itgss3  23304  dchreq  24700  axlowdimlem7  25546  axlowdimlem10  25549  padct  28691  resf1o  28699  locfinref  29042  indval2  29210  esummono  29249  gsumesum  29254  sigaclfu2  29317  measxun2  29406  measvuni  29410  measssd  29411  pmeasmono  29519  eulerpartlemt  29566  poimirlem9  32384  poimirlem15  32390  poimirlem25  32400  diophrw  36136  eldioph2lem1  36137  eldioph2lem2  36138  kelac1  36447  fsumsplit1  38436  ioccncflimc  38568  icocncflimc  38572  dirkercncflem2  38794  dirkercncflem3  38795  sge0ss  39102  meassle  39153  meadif  39169  meaiininclem  39173  isomenndlem  39217  hspmbllem1  39313  hspmbllem2  39314  ovolval4lem1  39336  fsumsplitsndif  40215