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

Metamath Proof Explorer

Theorem brrabga

Description: The law of concretion for operation class abstraction. (Contributed by Peter Mazsa, 24-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 brrabga.1 
 |-  ( ( x = A /\ y = B /\ z = C ) -> ( ph <-> ps ) )
2 brrabga.2 
 |-  R = { <. <. x , y >. , z >. | ph }
3 df-br 
 |-  ( <. A , B >. R C <-> <. <. A , B >. , C >. e. R )
4 2 eleq2i 
 |-  ( <. <. A , B >. , C >. e. R <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } )
5 3 4 bitri 
 |-  ( <. A , B >. R C <-> <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } )
6 1 eloprabga 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. <. A , B >. , C >. e. { <. <. x , y >. , z >. | ph } <-> ps ) )
7 5 6 bitrid 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> ( <. A , B >. R C <-> ps ) )