Let A means B in math logic.

Question

I am learning Math Logics to greatly reduce usage of words when defining patterns in math.

Currently I know what some basic signs means like $\implies$, $\iff$, $\forall$, $\exists$, $\exists!$, $:$, $:=$, etc.

Unfortunately couldn't find how to represent new ideas like "let A menas B".
Does such convetions exist ?

For example I would like to write :
Let $ B = f(A) $ means $B = \{ \forall a \in A : f(a) \}$,
where $A, B$ are sets, and $f$ is a function.

Can it be done as $B = f(A) \iff B = \{ \forall a \in A : f(a) \}$, or it's incorrect approach ?

---

EDIT $1$

After long day of learning math symbols I am close to believe that it's the correct notation :

$(B = f(A)) := (B = \{ b = f(a) : \forall a \in A \}$)

The reason is :
$:=$ means 'A is defined by B' so by it it's clear what I mean by suing set as a parameter to function

Please correct me if it's wrong.

Answer 1

I recommend very strong against the notation in "EDIT $1$". The "$:=$" symbol is really just "$=$" with an extra meaning. When we write "$\text{_____} := \text{_____}$", filling in the blank spaces on each side with something appropriate, we mean that the thing on the left is equal to the thing on the right by definition.

It's fine to say that a certain expression expressing a quantity is equal to another, but an equation does not express a quantity and it is not a good idea to set one equation "equal" to another equation.

In many cases, the correct mathematical notation for a statement is no notation. Here, for example, you could say,

We write $ B = f(A) $ if $B = \{ \forall a \in A : f(a) \}$.

---

The real problem with what you are trying to write, however, appears to be the use of the symbol $B$. When we write $B = f(A),$ there had better be no doubt about what the "$=$" symbol signifies: it says that whatever $B$ represents is exactly the same thing as whatever $f(A)$ represents.

What you actually seem to need to express in this case is, what exactly is the thing that $f(A)$ is meant to represent? That is, in order to say what $B = f(A)$ means, what you really need to do is just to describe what $f(A)$ means. That is, you need to define the notation "$f(A)$".

It seems that $A$ is intended to be a set in this particular context and $f$ is meant to be the name of a function. You could then define $f(A)$ like this:

For a set $A$ and a function $f: A\to X,$ $$ f(A) := \{ \forall a \in A : f(a) \}.$$

That's how the symbol "$:=$" can be used.