Theorem union_neutr

Proof
01. ⊢ A ∪ ∅ = ∅ ∪ A, union_comm.
union_neutr. ⊢ A ∪ ∅ = A, eq_trans 1 union_neutl.

Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.