Proving Vacuous Quantification in First-Order Logic

[Manchot]

I'm trying to prove a theorem which makes use of the identity $\exists x (P) \rightarrow P$ (where x is not a free variable of P). Intuitively, I want to believe it, but since I'm trying to do things rigorously, I'd like to be able to justify it to myself. Can anyone offer a suggestion as to how I'd derive the identifier from the usual axioms of first-order logic? (I'm sure that I'm missing something totally obvious). Thanks.

 

[fopc]

I don't understand. P is a naked propositional symbol in FOL? If so, then your done
(regardless of whether it has any quantifiers attached to it, or not). It's a tautology.

 

[Manchot]

P is a predicate in which x doesn't appear. Anyway, I know that it is a tautology, but I'm trying to prove it rigorously from FOL's axioms.

 

[Manchot]

Never mind, I've got it. Thanks anyway.