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 φ ψ
brrabga.2 R = x y z | φ
Assertion brrabga A V B W C X A B R C ψ

Proof

Step Hyp Ref Expression
1 brrabga.1 x = A y = B z = C φ ψ
2 brrabga.2 R = x y z | φ
3 df-br A B R C A B C R
4 2 eleq2i A B C R A B C x y z | φ
5 3 4 bitri A B R C A B C x y z | φ
6 1 eloprabga A V B W C X A B C x y z | φ ψ
7 5 6 syl5bb A V B W C X A B R C ψ