T318A
(Click "Prove" to run)
Prove Theorem:
(=> (and (exists ?X (f ?X)) (forall (?X ?Y) (=> (and (f ?X) (f ?Y)) (= ?X ?Y)))) (exists ?Y (forall ?X (<=> (f ?X) (= ?X ?Y)))))
Proof Trace