The One Point Rule is useful for dealing with existential quantifiers. It says that if you have an existentially quantified statement and part of it pins down an exact value for the quantified variable, then you can remove the quantification and replace the variable by the value whereever that variable appears in the rest of the statement.
Note the side condition that you must check before applying this rule: The variable, x, must not be free in the term, t, that you are using in the substitution.
For example, 
is
equivalent to 
. The first
conjunct checks that the term is member of the right set; it is usually
easy to discharge that check. Then, you are left with just the part
of the predicate in which the substitution has been made, e.g.,
.