Theorem bropabg

Description: Equivalence for two classes related by an ordered-pair class abstraction. A generalization of brsslt . (Contributed by RP, 26-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		bropabg.xA	|- ( x = A -> ( ph <-> ps ) )
2		bropabg.yB	|- ( y = B -> ( ps <-> ch ) )
3		bropabg.R	|- R = { <. x , y >. | ph }
4	3	bropaex12	|- ( A R B -> ( A e. _V /\ B e. _V ) )
5	1 2 3	brabg	|- ( ( A e. _V /\ B e. _V ) -> ( A R B <-> ch ) )
6	4 5	biadanii	|- ( A R B <-> ( ( A e. _V /\ B e. _V ) /\ ch ) )