Proof 01. 1 ⊢ (x, y1) ∈ ∅, hypo. 02. 2 ⊢ (x, y2) ∈ ∅, hypo. 03. 1 ⊢ y1 = y2, empty_efq 1. 04. 1, 2 ⊢ y1 = y2, wk 3. 05. ⊢ (x, y1) ∈ ∅ → (x, y2) ∈ ∅ → y1 = y2, subj_intro_ii 4. 06. ⊢ ∀y2. (x, y1) ∈ ∅ → (x, y2) ∈ ∅ → y1 = y2, uq_intro 5. 07. ⊢ ∀y1. ∀y2. (x, y1) ∈ ∅ → (x, y2) ∈ ∅ → y1 = y2, uq_intro 6. 08. ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ ∅ → (x, y2) ∈ ∅ → y1 = y2, uq_intro 7. empty_function. ⊢ function ∅, function_intro empty_relation 8.
Dependencies
The given proof depends on three axioms:
comp, efq, eq_subst.