Theorem undif 4437

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3895   ∖ cdif 4045   ∪ cun 4149

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279

This theorem is used by:  raldifeq  4448  pwundif  4582  imadifssranOLDOLD  6203  fveqf1o  7310  undifixp  8965  dfdom2  9008  sbthlem5  9113  sbthlem6  9114  domunsn  9149  fodomr  9150  mapdom2  9170  limensuci  9175  findcard2  9183  ssfi  9191  fodomfir  9322  marypha1lem  9428  brwdom2  9570  infdifsn  9661  ackbij1lem12  10311  ackbij1lem18  10317  ssfin4  10391  fin23lem28  10421  fin23lem30  10423  fin1a2lem13  10493  canthp1lem1  10740  indval2  12328  xrsupss  13442  xrinfmss  13443  hashssdif  14560  hashfun  14585  hashf1lem2  14604  fsumsplit1  15916  fsumless  15968  incexclem  16010  incexc  16011  fprodsplit1f  16162  pwssplit1  21339  frlmsslss2  22086  selvvvval  22456  mdetdiaglem  22918  mdetrlin  22922  mdetrsca  22923  mdetralt  22928  smadiadet  22990  isclo  23410  cmpcld  23725  rrxcph  25718  rrxdstprj1  25735  uniiccmbl  25916  itgss3  26140  dchreq  27590  noextendseq  28029  madeun  28275  axlowdimlem7  29531  axlowdimlem10  29534  fressupp  33328  padct  33357  resf1o  33368  fprodeq02  33461  gsummptres2  33660  cycpmcl  33723  cycpmco2  33740  cyc3co2  33747  cycpmconjslem2  33762  cyc3conja  33764  elrspunidl  34024  lbsdiflsp0  34304  dimkerim  34305  locfinref  34519  esummono  34732  gsumesum  34737  sigaclfu2  34799  measxun2  34889  measvuni  34893  measssd  34894  pmeasmono  35002  eulerpartlemt  35049  tgoldbachgtde  35335  satfvsucsuc  36216  poimirlem9  38640  poimirlem15  38646  poimirlem25  38656  evlselv  43710  fsuppssind  43714  diophrw  43863  eldioph2lem1  43864  eldioph2lem2  43865  kelac1  44158  tfsconcatfn  44433  tfsconcatrev  44443  ioccncflimc  46988  icocncflimc  46992  dirkercncflem2  47207  dirkercncflem3  47208  sge0ss  47515  meassle  47566  meadif  47582  meaiininclem  47589  isomenndlem  47633  hspmbllem1  47729  hspmbllem2  47730  ovolval4lem1  47752  fsumsplitsndif  48544  stgrclnbgr0  49156