Theorem abpr

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

	Ref	Expression
Assertion	abpr	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 , 𝑍 } ↔ ∀ 𝑥 ( 𝜑 ↔ ( 𝑥 = 𝑌 ∨ 𝑥 = 𝑍 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfpr2	⊢ { 𝑌 , 𝑍 } = { 𝑥 ∣ ( 𝑥 = 𝑌 ∨ 𝑥 = 𝑍 ) }
2	1	abeqabi	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 , 𝑍 } ↔ ∀ 𝑥 ( 𝜑 ↔ ( 𝑥 = 𝑌 ∨ 𝑥 = 𝑍 ) ) )