Theorem abpr

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

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

Proof

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