Theorem abtp

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

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

Proof

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