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 { <. x , y >. | ph } y <-> ph )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( x { <. x , y >. | ph } y <-> <. x , y >. e. { <. x , y >. | ph } )
2		opabidw	|- ( <. x , y >. e. { <. x , y >. | ph } <-> ph )
3	1 2	bitri	|- ( x { <. x , y >. | ph } y <-> ph )