# Why to define formulas defined using WFFs as WFFs?

The rules of formation for the language of set theory are the following:

1. If $$a$$ is a variable and $$b$$ is a variabe, then $$a\,{\in}\,b$$ is a WFF.

2. If $$P$$ is a WFF and $$Q$$ is a WFF, then $${\lnot}P$$,$$P{\land}Q$$,$$P{\lor}Q$$,$$P{\implies}Q$$,$$P{\iff}Q$$ are all WFFs.

3. If $$a$$ is a variable and $$P$$ is a WFF, then $${\forall}a(P)$$ and $${\exists}a:(P)$$ are WFFs.

Although point 1. is easy to understand, I have problems regarding 2. and 3. Why do things like $$P{\iff}Q$$ need to be defined as WFFs? Considering that $$P{\iff}Q$$ means that $$(P{\implies}Q){\land}(Q{\implies}P)$$, isn't it enough to just say that $$P{\land}Q$$ and $$P{\implies}Q$$ are WFFs and not mention $$P{\iff}Q$$ at all?

Having said that: YES, it is possible to "save" conncetives using only, e.g. $\lnot$ and $\land$ as primitive and introduce the others: $\lor, \to, \leftrightarrow$ as abbreviations through the usual definitions.
In the same way, we can use only $\forall$ as primitive and define $\exists$ as $\lnot \forall \lnot$.