View source for Definitions and iff

{{Stub page|grade=A|msg=Created quickly to provide some insight}}
__TOC__
==Purpose of "definitions"==
Suppose we make the following definition: 
* An {{M|X}} is {{M|D}} when it satisfies {{M|P(X)}} (for some statement {{M|P}}), symbolically:
** {{M|1=\forall X[P(X)\implies D]}}
We note this can be directly used to show {{M|X}} is {{M|D}} (we show {{M|X}} satisfies {{M|P}}, or some property equivalent to or implying {{M|P}}, thus it is {{M|D}})

But also we use definitions as follows:
* "Let {{M|X}} be {{M|D}}" to mean {{M|P(X)}} is true. Symbolically:
** {{M|1=\forall X[D\implies P(X)]}}


We see immediately: 
* {{M|1=\forall X[D\iff P(X)]}}
This makes perfect sense, as we'd want definitions to be equivalent to having some ''defined'' properties. 

'''Thus: {{M|X}} is {{M|D}} {{iff}} {{M|P(X)}} holds'''
==Examples==
Let {{M|X}} be (whatever), we say {{M|X}} is {{M|D}} if:
* {{M|P(X)}} holds.

We get both:
# If we have a {{M|Y}} for which {{M|P(Y)}} holds {{M|\implies}} {{M|Y}} is a {{M|D}}
# Let {{M|Y}} be a {{M|D}} {{M|\implies}} {{M|P(Y)}} holds
[[Category:Meta]]