# Metamath Proof Explorer

## Theorem brabga

Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses opelopabga.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({\phi }↔{\psi }\right)$
brabga.2 ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}$
Assertion brabga ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}{R}{B}↔{\psi }\right)$

### Proof

Step Hyp Ref Expression
1 opelopabga.1 ${⊢}\left({x}={A}\wedge {y}={B}\right)\to \left({\phi }↔{\psi }\right)$
2 brabga.2 ${⊢}{R}=\left\{⟨{x},{y}⟩|{\phi }\right\}$
3 df-br ${⊢}{A}{R}{B}↔⟨{A},{B}⟩\in {R}$
4 2 eleq2i ${⊢}⟨{A},{B}⟩\in {R}↔⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}$
5 3 4 bitri ${⊢}{A}{R}{B}↔⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}$
6 1 opelopabga ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left(⟨{A},{B}⟩\in \left\{⟨{x},{y}⟩|{\phi }\right\}↔{\psi }\right)$
7 5 6 syl5bb ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \left({A}{R}{B}↔{\psi }\right)$