This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V → A ⊔︀ ∅ ≈ A

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 in0 ⊢ A ∩ ∅ = ∅
3 endjudisj ⊢ A ∈ V ∧ ∅ ∈ V ∧ A ∩ ∅ = ∅ → A ⊔︀ ∅ ≈ A ∪ ∅
4 1 2 3 mp3an23 ⊢ A ∈ V → A ⊔︀ ∅ ≈ A ∪ ∅
5 un0 ⊢ A ∪ ∅ = A
6 4 5 breqtrdi ⊢ A ∈ V → A ⊔︀ ∅ ≈ A