Theorem brabd0

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by BJ, 17-Dec-2023)

	Ref	Expression
Hypotheses	brabd0.x	|- ( ph -> A. x ph )
	brabd0.y	|- ( ph -> A. y ph )
	brabd0.xch	|- ( ph -> F/ x ch )
	brabd0.ych	|- ( ph -> F/ y ch )
	brabd0.exa	|- ( ph -> A e. U )
	brabd0.exb	|- ( ph -> B e. V )
	brabd0.def	|- ( ph -> R = { <. x , y >. | ps } )
	brabd0.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion	brabd0	|- ( ph -> ( A R B <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		brabd0.x	|- ( ph -> A. x ph )
2		brabd0.y	|- ( ph -> A. y ph )
3		brabd0.xch	|- ( ph -> F/ x ch )
4		brabd0.ych	|- ( ph -> F/ y ch )
5		brabd0.exa	|- ( ph -> A e. U )
6		brabd0.exb	|- ( ph -> B e. V )
7		brabd0.def	|- ( ph -> R = { <. x , y >. | ps } )
8		brabd0.is	|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
9		df-br	|- ( A R B <-> <. A , B >. e. R )
10	7	eleq2d	|- ( ph -> ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ps } ) )
11	9 10	syl5bb	|- ( ph -> ( A R B <-> <. A , B >. e. { <. x , y >. | ps } ) )
12	1 2 3 4 5 6 8	opelopabd	|- ( ph -> ( <. A , B >. e. { <. x , y >. | ps } <-> ch ) )
13	11 12	bitrd	|- ( ph -> ( A R B <-> ch ) )