Theorem empty_efq

Proof
01. 1 ⊢ x ∈ ∅, hypo.
02. 1 ⊢ x ∈ {x | ⊥}, eq_subst empty_set_eq 1.
03. 1 ⊢ ⊥, comp_elim 2.
04. 1 ⊢ A, efq 3.
empty_efq. ⊢ x ∈ ∅ → A, subj_intro 4.

Dependencies
The given proof depends on three axioms:
comp, efq, eq_subst.