Metamath Proof Explorer

Theorem abtp

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

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

Proof

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