Theorem undif 4431

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∖ cdif 3895   ∪ cun 3896   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283

This theorem is referenced by:  undifrOLD  4433  raldifeq  4443  pwundif  4573  imadifssran  6103  fveqf1o  7242  undifixp  8864  dfdom2  8907  sbthlem5  9011  sbthlem6  9012  domunsn  9047  fodomr  9048  mapdom2  9068  limensuci  9073  findcard2  9081  ssfi  9089  fodomfir  9219  marypha1lem  9324  brwdom2  9466  infdifsn  9554  ackbij1lem12  10128  ackbij1lem18  10134  ssfin4  10208  fin23lem28  10238  fin23lem30  10240  fin1a2lem13  10310  canthp1lem1  10550  xrsupss  13210  xrinfmss  13211  hashssdif  14321  hashfun  14346  hashf1lem2  14365  fsumsplit1  15654  fsumless  15705  incexclem  15745  incexc  15746  fprodsplit1f  15899  pwssplit1  20995  frlmsslss2  21714  mdetdiaglem  22514  mdetrlin  22518  mdetrsca  22519  mdetralt  22524  smadiadet  22586  isclo  23003  cmpcld  23318  rrxcph  25320  rrxdstprj1  25337  uniiccmbl  25519  itgss3  25744  dchreq  27197  noextendseq  27607  madeun  27830  axlowdimlem7  28928  axlowdimlem10  28931  fressupp  32673  padct  32705  resf1o  32717  fprodeq02  32811  indval2  32840  gsummptres2  33040  cycpmcl  33092  cycpmco2  33109  cyc3co2  33116  cycpmconjslem2  33131  cyc3conja  33133  elrspunidl  33400  lbsdiflsp0  33660  dimkerim  33661  locfinref  33875  esummono  34088  gsumesum  34093  sigaclfu2  34155  measxun2  34244  measvuni  34248  measssd  34249  pmeasmono  34358  eulerpartlemt  34405  tgoldbachgtde  34694  satfvsucsuc  35430  poimirlem9  37690  poimirlem15  37696  poimirlem25  37706  selvvvval  42704  evlselv  42706  fsuppssind  42712  diophrw  42877  eldioph2lem1  42878  eldioph2lem2  42879  kelac1  43181  tfsconcatfn  43456  tfsconcatrev  43466  ioccncflimc  46008  icocncflimc  46012  dirkercncflem2  46227  dirkercncflem3  46228  sge0ss  46535  meassle  46586  meadif  46602  meaiininclem  46609  isomenndlem  46653  hspmbllem1  46749  hspmbllem2  46750  ovolval4lem1  46772  fsumsplitsndif  47498  stgrclnbgr0  48090