Theorem undif 4193

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

Syntax hints:   ↔ wb 196   = wceq 1632   ∖ cdif 3712   ∪ cun 3713   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059

This theorem is referenced by:  raldifeq  4203  difsnid  4486  fveqf1o  6721  ralxpmap  8075  undifixp  8112  dfdom2  8149  sbthlem5  8241  sbthlem6  8242  domunsn  8277  fodomr  8278  mapdom2  8298  limensuci  8303  findcard2  8367  unfi  8394  marypha1lem  8506  brwdom2  8645  infdifsn  8729  ackbij1lem12  9265  ackbij1lem18  9271  ssfin4  9344  fin23lem28  9374  fin23lem30  9376  fin1a2lem13  9446  canthp1lem1  9686  xrsupss  12352  xrinfmss  12353  hashssdif  13412  hashfun  13436  hashf1lem2  13452  fsumless  14747  incexclem  14787  incexc  14788  fprodsplit1f  14940  pwssplit1  19281  frlmsslss2  20336  mdetdiaglem  20626  mdetrlin  20630  mdetrsca  20631  mdetralt  20636  smadiadet  20698  isclo  21113  cmpcld  21427  rrxcph  23400  rrxdstprj1  23412  uniiccmbl  23578  itgss3  23800  dchreq  25203  axlowdimlem7  26048  axlowdimlem10  26051  padct  29827  resf1o  29835  fprodeq02  29899  locfinref  30238  indval2  30406  esummono  30446  gsumesum  30451  sigaclfu2  30514  measxun2  30603  measvuni  30607  measssd  30608  pmeasmono  30716  eulerpartlemt  30763  tgoldbachgtde  31068  noextendseq  32147  poimirlem9  33749  poimirlem15  33755  poimirlem25  33765  diophrw  37842  eldioph2lem1  37843  eldioph2lem2  37844  kelac1  38153  fsumsplit1  40325  ioccncflimc  40619  icocncflimc  40623  dirkercncflem2  40842  dirkercncflem3  40843  sge0ss  41150  meassle  41201  meadif  41217  meaiininclem  41224  isomenndlem  41268  hspmbllem1  41364  hspmbllem2  41365  ovolval4lem1  41387  fsumsplitsndif  41871