Theorem opelopabbv

Description: Membership of an ordered pair in a class abstraction of ordered pairs, biconditional form. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	opelopabbv.def	|- ( ph -> R = { <. x , y >. | ps } )
	opelopabbv.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion	opelopabbv	|- ( ph -> ( <. A , B >. e. R <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		opelopabbv.def	|- ( ph -> R = { <. x , y >. | ps } )
2		opelopabbv.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
3	1	eleq2d	|- ( ph -> ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ps } ) )
4		ax-5	|- ( ph -> A. x ph )
5		ax-5	|- ( ph -> A. y ph )
6		nfvd	|- ( ph -> F/ x ch )
7		nfvd	|- ( ph -> F/ y ch )
8	4 5 6 7 2	opelopabb	|- ( ph -> ( <. A , B >. e. { <. x , y >. | ps } <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )
9	3 8	bitrd	|- ( ph -> ( <. A , B >. e. R <-> ( ( A e. _V /\ B e. _V ) /\ ch ) ) )