Metamath Proof Explorer

Theorem brabgaf

Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013) (Revised by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses brabgaf.0 
|- F/ x ps
brabgaf.1 
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
brabgaf.2 
|- R = { <. x , y >. | ph }
Assertion brabgaf 
|- ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )

Proof

Step Hyp Ref Expression
1 brabgaf.0 
 |-  F/ x ps
2 brabgaf.1 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
3 brabgaf.2 
 |-  R = { <. x , y >. | ph }
4 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
5 3 eleq2i 
 |-  ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ph } )
6 4 5 bitri 
 |-  ( A R B <-> <. A , B >. e. { <. x , y >. | ph } )
7 elopab 
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) )
8 elisset 
 |-  ( A e. V -> E. x x = A )
9 elisset 
 |-  ( B e. W -> E. y y = B )
10 exdistrv 
 |-  ( E. x E. y ( x = A /\ y = B ) <-> ( E. x x = A /\ E. y y = B ) )
11 nfe1 
 |-  F/ x E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
12 11 1 nfbi 
 |-  F/ x ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
13 nfe1 
 |-  F/ y E. y ( <. A , B >. = <. x , y >. /\ ph )
14 13 nfex 
 |-  F/ y E. x E. y ( <. A , B >. = <. x , y >. /\ ph )
15 nfv 
 |-  F/ y ps
16 14 15 nfbi 
 |-  F/ y ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps )
17 opeq12 
 |-  ( ( x = A /\ y = B ) -> <. x , y >. = <. A , B >. )
18 copsexgw 
 |-  ( <. A , B >. = <. x , y >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
19 18 eqcoms 
 |-  ( <. x , y >. = <. A , B >. -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
20 17 19 syl 
 |-  ( ( x = A /\ y = B ) -> ( ph <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) ) )
21 20 2 bitr3d 
 |-  ( ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
22 16 21 exlimi 
 |-  ( E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
23 12 22 exlimi 
 |-  ( E. x E. y ( x = A /\ y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
24 10 23 sylbir 
 |-  ( ( E. x x = A /\ E. y y = B ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
25 8 9 24 syl2an 
 |-  ( ( A e. V /\ B e. W ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ph ) <-> ps ) )
26 7 25 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) )
27 6 26 bitrid 
 |-  ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )