Metamath Proof Explorer

Theorem abpr

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

Ref Expression
Assertion abpr 
|- ( { x | ph } = { Y , Z } <-> A. x ( ph <-> ( x = Y \/ x = Z ) ) )

Proof

Step Hyp Ref Expression
1 dfpr2 
 |-  { Y , Z } = { x | ( x = Y \/ x = Z ) }
2 1 abeqabi 
 |-  ( { x | ph } = { Y , Z } <-> A. x ( ph <-> ( x = Y \/ x = Z ) ) )