Theorem brab2a

Description: The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		brab2a.1	|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2		brab2a.2	|- R = { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) }
3		opabssxp	|- { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } C_ ( C X. D )
4	2 3	eqsstri	|- R C_ ( C X. D )
5	4	brel	|- ( A R B -> ( A e. C /\ B e. D ) )
6		df-br	|- ( A R B <-> <. A , B >. e. R )
7	2	eleq2i	|- ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } )
8	6 7	bitri	|- ( A R B <-> <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } )
9	1	opelopab2a	|- ( ( A e. C /\ B e. D ) -> ( <. A , B >. e. { <. x , y >. | ( ( x e. C /\ y e. D ) /\ ph ) } <-> ps ) )
10	8 9	bitrid	|- ( ( A e. C /\ B e. D ) -> ( A R B <-> ps ) )
11	5 10	biadanii	|- ( A R B <-> ( ( A e. C /\ B e. D ) /\ ps ) )