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	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow ⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}$$
2		opabidw	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
3	1 2	bitri	$$⊢x\left\{⟨x,y⟩|\phi \right\}y\leftrightarrow \phi$$