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

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 ⊢ x = A ∧ y = B → φ ↔ ψ
brabga.2 ⊢ R = x y | φ
Assertion brabga ⊢ A ∈ V ∧ B ∈ W → A R B ↔ ψ

Proof

Step Hyp Ref Expression
1 opelopabga.1 ⊢ x = A ∧ y = B → φ ↔ ψ
2 brabga.2 ⊢ R = x y | φ
3 df-br ⊢ A R B ↔ A B ∈ R
4 2 eleq2i ⊢ A B ∈ R ↔ A B ∈ x y | φ
5 3 4 bitri ⊢ A R B ↔ A B ∈ x y | φ
6 1 opelopabga ⊢ A ∈ V ∧ B ∈ W → A B ∈ x y | φ ↔ ψ
7 5 6 bitrid ⊢ A ∈ V ∧ B ∈ W → A R B ↔ ψ