Theorem dju0en

Description: Cardinal addition with cardinal zero (the empty set). Part (a1) of proof of Theorem 6J of Enderton p. 143. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	dju0en	$$⊢A\in V\to \left(A\mathrm{\bigsqcup ︀}\varnothing \right)\approx A$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2		in0	$$⊢A\cap \varnothing =\varnothing$$
3		endjudisj	$$⊢\left(A\in V\wedge \varnothing \in \mathrm{V}\wedge A\cap \varnothing =\varnothing \right)\to \left(A\mathrm{\bigsqcup ︀}\varnothing \right)\approx \left(A\cup \varnothing \right)$$
4	1 2 3	mp3an23	$$⊢A\in V\to \left(A\mathrm{\bigsqcup ︀}\varnothing \right)\approx \left(A\cup \varnothing \right)$$
5		un0	$$⊢A\cup \varnothing =A$$
6	4 5	breqtrdi	$$⊢A\in V\to \left(A\mathrm{\bigsqcup ︀}\varnothing \right)\approx A$$