Question about the proof that $A = B \implies \{A, B\} = \{A \}$ I'm trying to do it as a 100% explicit proof, and I have a couple of questions. Here's the proof:
Suppose $A,B$ are sets, and suppose $A=B$, and suppose $\gamma \neq \varnothing$ and $\gamma \in \{A,B\}$.
$\implies \gamma = A \lor \gamma = B$
$\gamma = B \iff \gamma = A$
$\implies \gamma = A \lor \gamma = A$
$\implies \gamma = A$
$\therefore\gamma \in \{A\}$
Suppose instead $\gamma \in \{A\}$.
$\implies \gamma = A \lor \gamma = \varnothing$
$\gamma \neq \varnothing$
$\implies \gamma = A$
$\implies \gamma = A \lor \gamma = A$
$\gamma = A \iff \gamma = B$
$\implies \gamma  = A \lor \gamma = B$
$\therefore \gamma \in  \{A,B\}$
$\therefore A = B \implies \{A,B\} = \{A \}$
Some questions about the proof:

*

*Is it correct?

*My main problem is that although I'm trying to do a 100% explicit proof, I'm unable to determine when I'm actually stating a tautology which doesn't advance the proof in any way. For example, it seems to me that normally $A = B$ directly implies $\{A,B\} = \{A,A\}$, but at the same time, it feels to me like this doesn't necessarily follow, since I was able to write a step-by-step transformation of the one into the other. What exactly are the assumptions necessary to be able to get a direct implication from $A=B$ to $\{A,B\} = \{A,A\}$? Is it a syntactical thing?

*Under what syntactical and first-order assumptions does $\gamma \in \{A,B\}$ mean (or imply?) $\gamma = A \lor \gamma = B$? It has been suggested in the comments that actually, any disjunction is infinitely long, but under what assumptions is this the case?

Any suggestions, reading recommendations, or answers, are very highly appreciated!
 A: If $A=B$, then $\{A,B\}=\{A\}$ which is almost not necessary to be proved.

*

*If what you chose is naive set theory, then the conclusion conclude clearly from the naive definition of sets. In Cantor's words, a set is a gathering together into a whole of definite, distinct objects of our perception or our thought. This means that sets have three property: (1) elements are definite; (2) elements are distinct; (3) elements have no orders.

*If what you chose is axiomatic set theory, then the conclusion conclude easily from Axiom of Extension: For any sets $x,y$, if for any sets $z$ we have $z\in x$ if and only if $z\in y$ then $x=y$, i.e., $\forall x,y(\forall z(z\in x\leftrightarrow z\in y)\to x=y))$.


By the way, if you still want to check whether your proof method is right or not, the following may be a reference.
Proof 1. This because
$$
\begin{array}{rcll}
x\in\{A,B\}&\iff&x=A~\text{or}~x=B&\\
&\iff&x=A~\text{or}~x=A&\text{by}~A=B\\
&\iff&x=A&\text{by}~(\varphi\vee\varphi)\leftrightarrow\varphi\\
&\iff&x\in\{A\}.&
\end{array}
$$
Remark. Although Proof 1 is also right, but it's a detour and not necessary since $\{A,A\}=\{A\}$ is obvious. I think what you focused is not how to prove it in a clear and neat way but whether your own proof method is right or not.

If a proof is necessary, I think the following is better.
Proof 2. Suppose $A=B$. Then $\{A,B\}=\{A,A\}=\{A\}$ as desired.
