∃x:τ.P(x) just means there is some P in which x is used for which there exists some x such that P is true. τ is the type of x, which is really important in the type theory, but you can think of it as sorta-kinda just specifying a set of elements from which we know the x is chosen.
no subject
∃x:τ.P(x) just means there is some P in which x is used for which there exists some x such that P is true. τ is the type of x, which is really important in the type theory, but you can think of it as sorta-kinda just specifying a set of elements from which we know the x is chosen.