compl_intro

Theorem compl_intro

Theorem. compl_intro
set x → ¬x ∈ A → x ∈ compl A

Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ ¬x ∈ A, hypo.
03. 1, 2 ⊢ x ∈ {x | ¬x ∈ A}, comp_intro 1 2.
04. 1, 2 ⊢ x ∈ compl A, eq_subst_rev compl_eq 3, P u ↔ x ∈ u.
compl_intro. ⊢ set x → ¬x ∈ A → x ∈ compl A, subj_intro_ii 4.

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