I'm trying to prove a theorem which makes use of the identity [itex]\exists x (P) \rightarrow P[/itex] (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.