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

Metamath Proof Explorer

Theorem brabsb

Description: The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008)

Ref Expression
Hypothesis brabsb.1 ⊢ R = x y | φ
Assertion brabsb ⊢ A R B ↔ [˙A / x]˙ [˙B / y]˙ φ

Proof

Step Hyp Ref Expression
1 brabsb.1 ⊢ R = x y | φ
2 df-br ⊢ A R B ↔ A B ∈ R
3 1 eleq2i ⊢ A B ∈ R ↔ A B ∈ x y | φ
4 opelopabsb ⊢ A B ∈ x y | φ ↔ [˙A / x]˙ [˙B / y]˙ φ
5 2 3 4 3bitri ⊢ A R B ↔ [˙A / x]˙ [˙B / y]˙ φ