This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )