Theorem undifr 4449

Description: Union of complementary parts into whole. Commuted form of undifr 4449. (Contributed by Thierry Arnoux, 21-Nov-2023.) (Proof shortened by SN, 11-Mar-2025.)

Assertion

Ref	Expression
undifr	⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)

Proof of Theorem undifr

Step	Hyp	Ref	Expression
1		ssequn2 4145	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
2		undif1 4440	. . 3 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2771	. 2 ⊢ (((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitr4i 281	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∖ cdif 3905   ∪ cun 3906   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290

This theorem is used by:  difsnid  4781  f1ofvswap  7315  ralxpmap  8903  selvvvval  22330  psdmullem  22365  psdmul  22366  tocyc01  33469  rprmdvdsprod  33855  evlextv  33963  esplyind  33996  esplyindfv  33997  vietalem  34000  aks6d1c5lem3  42945  evlselvlem  43361  evlselv  43362  isubgr3stgrlem3  48774