undif3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > undif3		Structured version Visualization version Unicode version

Theorem undif3 3888

Description: An equality involving class union and class difference. The first equality of Exercise 13 of [TakeutiZaring] p. 22. (Contributed by Alan Sare, 17-Apr-2012.) (Proof shortened by JJ, 13-Jul-2021.)

**Assertion**
Ref	Expression
undif3	$\$ $\$ $\$

Proof of Theorem undif3 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elun 3753	. . . 4 $\/$
2		pm4.53 513	. . . . 5 $/\$ $\/$
3		eldif 3584	. . . . 5 $\$ $/\$
4	2, 3	xchnxbir 323	. . . 4 $\$ $\/$
5	1, 4	anbi12i 733	. . 3 $/\$ $\$ $\/$ $/\$ $\/$
6		eldif 3584	. . 3 $\$ $\$ $/\$ $\$
7		elun 3753	. . . 4 $\$ $\/$ $\$
8		eldif 3584	. . . . 5 $\$ $/\$
9	8	orbi2i 541	. . . 4 $\/$ $\$ $\/$ $/\$
10		ordi 908	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$
11		orcom 402	. . . . . 6 $\/$ $\/$
12	11	anbi2i 730	. . . . 5 $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
13	10, 12	bitri 264	. . . 4 $\/$ $/\$ $\/$ $/\$ $\/$
14	7, 9, 13	3bitri 286	. . 3 $\$ $\/$ $/\$ $\/$
15	5, 6, 14	3bitr4ri 293	. 2 $\$ $\$ $\$
16	15	eqriv 2619	1 $\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3 $\/$ wo 383 $/\$ wa 384

wceq 1483

wcel 1990 $\$ cdif 3571

cun 3572

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-dif 3577 df-un 3579

This theorem is referenced by: undifabs 4045 llycmpkgen2 21353 hgt750lemb 30734

W3C validator