Fuente TeX:

\infer[I_\exists]{(\exists y)(P(x,y) \land \lnot y =' f(x))}{P(x,g(x)) \land \lnot g(x) =' f(x)}