Theorem abtp

Description: Condition for a class abstraction to be a triple. (Contributed by RP, 25-Aug-2024)

	Ref	Expression
Assertion	abtp	$$⊢\left\{x|\phi \right\}=\left\{X,Y,Z\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \left(x=X\vee x=Y\vee x=Z\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dftp2	$$⊢\left\{X,Y,Z\right\}=\left\{x|\left(x=X\vee x=Y\vee x=Z\right)\right\}$$
2	1	abeqabi	$$⊢\left\{x|\phi \right\}=\left\{X,Y,Z\right\}\leftrightarrow \forall x\left(\phi \leftrightarrow \left(x=X\vee x=Y\vee x=Z\right)\right)$$