Theorem bj-brab2a1

Description: "Unbounded" version of brab2a . (Contributed by BJ, 25-Dec-2023)

	Ref	Expression
Hypotheses	bj-brab2a1.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
	bj-brab2a1.2	|- R = { <. x , y >. | ph }
Assertion	bj-brab2a1	|- ( A R B <-> ( ( A e. _V /\ B e. _V ) /\ ps ) )

Proof

Step	Hyp	Ref	Expression
1		bj-brab2a1.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2		bj-brab2a1.2	|- R = { <. x , y >. | ph }
3		vex	|- x e. _V
4		vex	|- y e. _V
5	3 4	pm3.2i	|- ( x e. _V /\ y e. _V )
6	5	biantrur	|- ( ph <-> ( ( x e. _V /\ y e. _V ) /\ ph ) )
7	6	opabbii	|- { <. x , y >. | ph } = { <. x , y >. | ( ( x e. _V /\ y e. _V ) /\ ph ) }
8	2 7	eqtri	|- R = { <. x , y >. | ( ( x e. _V /\ y e. _V ) /\ ph ) }
9	1 8	brab2a	|- ( A R B <-> ( ( A e. _V /\ B e. _V ) /\ ps ) )