I have a problem I'm working on that I'm a bit stuck on. In this problem we are allowed to use Taut Con in our Fitch proof. The goal is to prove the following from no premises: ~∃x∀y ( P(x,y) ↔ ~P(y,y)) My initial thought is to begin a subproof with the problem itself, except without the negation, that way if I ultimately conclude in a falsum, I can use negation introduction on the last step to get the goal. Within this subproof I'd imagine to want to use a subproof for Existential elimination, that way I can work with ∀y ( P(a,y) ↔ ~P(y,y)) and using universal elimination get ( P(a,b) ↔ ~P(b,b)). Then if I can prove this biconditional statement to be a contradiction/falsum, I can use existential elimination on the beginning of the subproof to get out of it and use the falsum in my original plan. I know I'm allowed to use Taut Con but not sure how to apply it to ( P(a,b) ↔ ~P(b,b)) in order to prove it to lead to a contradiction. Any help is much appreciated.