incl_antisym

Theorem incl_antisym

Theorem. incl_antisym
A ⊆ B → B ⊆ A → A = B

Proof
01. 1 ⊢ A ⊆ B, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 1, 2 ⊢ x ∈ B, incl_elim 1 2.
04. 1 ⊢ x ∈ A → x ∈ B, subj_intro 3.
05. 5 ⊢ B ⊆ A, hypo.
06. 6 ⊢ x ∈ B, hypo.
07. 5, 6 ⊢ x ∈ A, incl_elim 5 6.
08. 5 ⊢ x ∈ B → x ∈ A, subj_intro 7.
09. 1, 5 ⊢ x ∈ A ↔ x ∈ B, bij_intro 4 8.
10. 1, 5 ⊢ ∀x. x ∈ A ↔ x ∈ B, uq_intro 9.
11. 1, 5 ⊢ A = B, ext 10.
incl_antisym. ⊢ A ⊆ B → B ⊆ A → A = B, subj_intro_ii 11.

Dependencies
The given proof depends on one axiom:
ext.