Theorem bj-opelopabid

Description: Membership in an ordered-pair class abstraction. One can remove the DV condition on x , y by using opabid in place of opabidw . (Contributed by BJ, 22-May-2024)

	Ref	Expression
Assertion	bj-opelopabid	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } )
2		opabidw	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ↔ 𝜑 )
3	1 2	bitri	⊢ ( 𝑥 { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } 𝑦 ↔ 𝜑 )