Theorem undifr 4484

Description: Union of complementary parts into whole. (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 4183	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
2		undif1 4477	. . 3 ⊢ ((𝐵 ∖ 𝐴) ∪ 𝐴) = (𝐵 ∪ 𝐴)
3	2	eqeq1i 2732	. 2 ⊢ (((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵 ↔ (𝐵 ∪ 𝐴) = 𝐵)
4	1, 3	bitr4i 277	1 ⊢ (𝐴 ⊆ 𝐵 ↔ ((𝐵 ∖ 𝐴) ∪ 𝐴) = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1533   ∖ cdif 3944   ∪ cun 3945   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3429  df-v 3473  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325

This theorem is referenced by:  difsnid  4816  f1ofvswap  7319  ralxpmap  8919  psdmullem  22094  psdmul  22095  tocyc01  32857  aks6d1c5lem3  41612  selvvvval  41821  evlselvlem  41822  evlselv  41823