Theorem undif 4422

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 4126	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
2		undif2 4417	. . 3 ⊢ (𝐴 ∪ (𝐵 ∖ 𝐴)) = (𝐴 ∪ 𝐵)
3	2	eqeq1i 2741	. 2 ⊢ ((𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵 ↔ (𝐴 ∪ 𝐵) = 𝐵)
4	1, 3	bitr4i 278	1 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∪ (𝐵 ∖ 𝐴)) = 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1542   ∖ cdif 3886   ∪ cun 3887   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  raldifeq  4433  pwundif  4565  imadifssran  6115  fveqf1o  7257  undifixp  8882  dfdom2  8925  sbthlem5  9029  sbthlem6  9030  domunsn  9065  fodomr  9066  mapdom2  9086  limensuci  9091  findcard2  9099  ssfi  9107  fodomfir  9238  marypha1lem  9346  brwdom2  9488  infdifsn  9578  ackbij1lem12  10152  ackbij1lem18  10158  ssfin4  10232  fin23lem28  10262  fin23lem30  10264  fin1a2lem13  10334  canthp1lem1  10575  indval2  12164  xrsupss  13261  xrinfmss  13262  hashssdif  14374  hashfun  14399  hashf1lem2  14418  fsumsplit1  15707  fsumless  15759  incexclem  15801  incexc  15802  fprodsplit1f  15955  pwssplit1  21054  frlmsslss2  21755  mdetdiaglem  22563  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  smadiadet  22635  isclo  23052  cmpcld  23367  rrxcph  25359  rrxdstprj1  25376  uniiccmbl  25557  itgss3  25782  dchreq  27221  noextendseq  27631  madeun  27876  axlowdimlem7  29017  axlowdimlem10  29020  fressupp  32761  padct  32791  resf1o  32803  fprodeq02  32897  gsummptres2  33114  cycpmcl  33177  cycpmco2  33194  cyc3co2  33201  cycpmconjslem2  33216  cyc3conja  33218  elrspunidl  33488  lbsdiflsp0  33770  dimkerim  33771  locfinref  33985  esummono  34198  gsumesum  34203  sigaclfu2  34265  measxun2  34354  measvuni  34358  measssd  34359  pmeasmono  34468  eulerpartlemt  34515  tgoldbachgtde  34804  satfvsucsuc  35547  poimirlem9  37950  poimirlem15  37956  poimirlem25  37966  selvvvval  43018  evlselv  43020  fsuppssind  43026  diophrw  43191  eldioph2lem1  43192  eldioph2lem2  43193  kelac1  43491  tfsconcatfn  43766  tfsconcatrev  43776  ioccncflimc  46313  icocncflimc  46317  dirkercncflem2  46532  dirkercncflem3  46533  sge0ss  46840  meassle  46891  meadif  46907  meaiininclem  46914  isomenndlem  46958  hspmbllem1  47054  hspmbllem2  47055  ovolval4lem1  47077  fsumsplitsndif  47829  stgrclnbgr0  48441