Theorem dfun3

Description: Union defined in terms of intersection (De Morgan's law). Definition of union in Mendelson p. 231. (Contributed by NM, 8-Jan-2002)

	Ref	Expression
Assertion	dfun3	$$⊢A\cup B=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfun2	$$⊢A\cup B=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\setminus B\right)$$
2		dfin2	$$⊢\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus B\right)=\left(\mathrm{V}\setminus A\right)\setminus \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)\right)$$
3		ddif	$$⊢\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)=B$$
4	3	difeq2i	$$⊢\left(\mathrm{V}\setminus A\right)\setminus \left(\mathrm{V}\setminus \left(\mathrm{V}\setminus B\right)\right)=\left(\mathrm{V}\setminus A\right)\setminus B$$
5	2 4	eqtr2i	$$⊢\left(\mathrm{V}\setminus A\right)\setminus B=\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus B\right)$$
6	5	difeq2i	$$⊢\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\setminus B\right)=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus B\right)\right)$$
7	1 6	eqtri	$$⊢A\cup B=\mathrm{V}\setminus \left(\left(\mathrm{V}\setminus A\right)\cap \left(\mathrm{V}\setminus B\right)\right)$$