The following is a notation that I want to introduce to shorten writing of formulas in set theory, that idea is to use lower cases to indicate membership in upper case form of them, also use special abbreviation of the subset relation.
Formal Exposition:
Define: $\mathcal Q x(\phi(x)) \iff \mathcal Q x \in X (\phi(x))$
Define $\mathcal Q x'(\phi(x')) \iff \mathcal Q x' \not \in X (\phi(x'))$
Define: $[\mathcal Q x (\phi(x)) \ \texttt{-"-}] \iff [\mathcal Q x (\phi(x)) \land \mathcal Q x' (\neg\phi(x'))]$
Define: $\mathcal Q A^- \equiv_{df} \mathcal Q A^- \subseteq A$
Define: $A^- \subseteq A \iff \forall a^- (a^- \in A)$
Or can be written concealing $``\in"$ as:
$A^- \subseteq A \iff \forall a^- ( \exists a (a^- = a))$
Where $\mathcal Q$ is either $\forall$ or $\exists$ symbols.
Where $\phi(x')$ is the formula obtained from formula $\phi(x)$ by merely replacing all occurrences of the symbol $x$ in $\phi(x)$ by the symbol $x'$, and keeping all other symbols.
So lower case is used to signify membership, so a well formed formula that contains a symbol in lower case must contain its upper case form appearing somewhere in the formula before all of occurrences of the lower case form, while symbols written in upper case face no restrictions (a part form the above), so they can even be written alone (not followed by a lower case form of them).
Example: writing axioms of ZFC as:
Extensionality: $\forall X,Y ([\forall x (x \in Y) \ \texttt{-"-} ] \to X=Y)$
Empty:$\exists X \forall x (x\neq x)$
Pairing: $\forall A,B \exists X [\forall x (x=A \lor x=B) \ \texttt{-"-}]$
Boolean Union:$\forall A,B \exists X [\forall x (x \in A \lor x \in B) \ \texttt{-"-}]$
Set Union: $\forall A \exists X [\forall x (\exists a (x \in a) ) \ \texttt{-"-}] $
Power:$\forall A \exists X [\forall x (\exists A^- (x=A^-)) \ \texttt{-"-}]$
Separation: $\forall A \exists X [\forall x ( x \in A \land \phi(x)) \ \texttt{-"-}]$
Replacement: $\forall A ( \forall a \exists! S (\phi(a,S))\to\exists X [\forall x (\exists a (\phi(a,x))) \ \texttt{-"-}])$
With the use of identity we can conceal the symbol $\in$ altogether, examples are:
Extensionality:$\forall X,Y ([\forall x (\exists y (x=y))\ \texttt{-"-} ] \to X=Y)$
Boolean Union:$\forall A,B \exists X [\forall x (\exists a (x = a) \lor \exists b (x=b)) \ \texttt{-"-}]$
Set Union: $\forall A \exists X [\forall x (\exists a \exists B (a=B \land \exists b ( x=b)) ) \ \texttt{-"-}] $
Separation: $\forall A \exists X [\forall x (\exists a (x=a \land \phi(x))) \ \texttt{-"-}]$
However this is longer, but it gives the pseudo-appearance of set theory written in first order logic with identity!?
Question: had that been done before?
Question: is it found elegant?