Theorem equncomVD 44844

Description: If a class equals the union of two other classes, then it equals the union of those two classes commuted. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. equncom 4112 is equncomVD 44844 without virtual deductions and was automatically derived from equncomVD 44844.

1::	⊢ (   𝐴 = (𝐵 ∪ 𝐶)   ▶   𝐴 = (𝐵 ∪ 𝐶)   )
2::	⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
3:1,2:	⊢ (   𝐴 = (𝐵 ∪ 𝐶)   ▶   𝐴 = (𝐶 ∪ 𝐵)   )
4:3:	⊢ (𝐴 = (𝐵 ∪ 𝐶) → 𝐴 = (𝐶 ∪ 𝐵))
5::	⊢ (   𝐴 = (𝐶 ∪ 𝐵)   ▶   𝐴 = (𝐶 ∪ 𝐵)   )
6:5,2:	⊢ (   𝐴 = (𝐶 ∪ 𝐵)   ▶   𝐴 = (𝐵 ∪ 𝐶)   )
7:6:	⊢ (𝐴 = (𝐶 ∪ 𝐵) → 𝐴 = (𝐵 ∪ 𝐶))
8:4,7:	⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))

(Contributed by Alan Sare, 17-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
equncomVD	⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))

Proof of Theorem equncomVD

Step	Hyp	Ref	Expression
1		idn1 44551	. . . 4 ⊢ (   𝐴 = (𝐵 ∪ 𝐶)   ▶   𝐴 = (𝐵 ∪ 𝐶)   )
2		uncom 4111	. . . 4 ⊢ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)
3		eqeq1 2733	. . . . 5 ⊢ (𝐴 = (𝐵 ∪ 𝐶) → (𝐴 = (𝐶 ∪ 𝐵) ↔ (𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵)))
4	3	biimprd 248	. . . 4 ⊢ (𝐴 = (𝐵 ∪ 𝐶) → ((𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) → 𝐴 = (𝐶 ∪ 𝐵)))
5	1, 2, 4	e10 44671	. . 3 ⊢ (   𝐴 = (𝐵 ∪ 𝐶)   ▶   𝐴 = (𝐶 ∪ 𝐵)   )
6	5	in1 44548	. 2 ⊢ (𝐴 = (𝐵 ∪ 𝐶) → 𝐴 = (𝐶 ∪ 𝐵))
7		idn1 44551	. . . 4 ⊢ (   𝐴 = (𝐶 ∪ 𝐵)   ▶   𝐴 = (𝐶 ∪ 𝐵)   )
8		eqeq2 2741	. . . . 5 ⊢ ((𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) → (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵)))
9	8	biimprcd 250	. . . 4 ⊢ (𝐴 = (𝐶 ∪ 𝐵) → ((𝐵 ∪ 𝐶) = (𝐶 ∪ 𝐵) → 𝐴 = (𝐵 ∪ 𝐶)))
10	7, 2, 9	e10 44671	. . 3 ⊢ (   𝐴 = (𝐶 ∪ 𝐵)   ▶   𝐴 = (𝐵 ∪ 𝐶)   )
11	10	in1 44548	. 2 ⊢ (𝐴 = (𝐶 ∪ 𝐵) → 𝐴 = (𝐵 ∪ 𝐶))
12	6, 11	impbii 209	1 ⊢ (𝐴 = (𝐵 ∪ 𝐶) ↔ 𝐴 = (𝐶 ∪ 𝐵))

Syntax hints:   ↔ wb 206   = wceq 1540   ∪ cun 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-vd1 44547

This theorem is referenced by: (None)