Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 3 ⊢ set x, hypo.
04. 4 ⊢ ¬a = x, hypo.
05. 5 ⊢ y ∈ img {(a, b)} {x}, hypo.
06. 5 ⊢ ∃u. u ∈ {x} ∧ (u, y) ∈ {(a, b)}, img_elim 5.
07. 7 ⊢ u ∈ {x} ∧ (u, y) ∈ {(a, b)}, hypo.
08. 7 ⊢ u ∈ {x}, conj_eliml 7.
09. 3, 7 ⊢ u = x, sg_elim 3 8.
10. 1, 2 ⊢ set (a, b), set_pair 1 2.
11. 7 ⊢ (u, y) ∈ {(a, b)}, conj_elimr 7.
12. 1, 2, 7 ⊢ (u, y) = (a, b), sg_elim 10 11.
13. 1, 2, 7 ⊢ (a, b) = (u, y), eq_symm 12.
14. 1, 2, 7 ⊢ a = u ∧ b = y, pair_property 1 2 13.
15. 1, 2, 7 ⊢ a = u, conj_eliml 14.
16. 1, 2, 3, 7 ⊢ a = x, eq_trans 15 9.
17. 1, 2, 3, 5 ⊢ a = x, ex_elim 6 16.
18. 1, 2, 3, 4, 5 ⊢ ⊥, neg_elim 4 17.
19. 1, 2, 3, 4, 5 ⊢ y ∈ ∅, efq 18.
20. 1, 2, 3, 4 ⊢ y ∈ img {(a, b)} {x} → y ∈ ∅, subj_intro 19.
21. 1, 2, 3, 4 ⊢ ∀y. y ∈ img {(a, b)} {x} → y ∈ ∅, uq_intro 20.
22. 1, 2, 3, 4 ⊢ img {(a, b)} {x} ⊆ ∅, incl_intro 21.
23. ⊢ ∅ ⊆ img {(a, b)} {x}, empty_set_is_least.
24. 1, 2, 3, 4 ⊢ img {(a, b)} {x} = ∅, incl_antisym 22 23.
img_sg_sg_neq. ⊢ set a → set b → set x → ¬a = x →
img {(a, b)} {x} = ∅, subj_intro_iv 24.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.