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

Metamath Proof Explorer

Theorem brabg

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

	Ref	Expression
Hypotheses	opelopabg.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
	opelopabg.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
	brabg.5	$⊢ R = \{⟨x, y⟩ \| φ\}$
Assertion	brabg	$⊢ (A \in C \land B \in D) \to (A R B \leftrightarrow χ)$

Step	Hyp	Ref	Expression
1		opelopabg.1	$⊢ x = A \to (φ \leftrightarrow ψ)$
2		opelopabg.2	$⊢ y = B \to (ψ \leftrightarrow χ)$
3		brabg.5	$⊢ R = \{⟨x, y⟩ \| φ\}$
4	1 2	sylan9bb	$⊢ (x = A \land y = B) \to (φ \leftrightarrow χ)$
5	4 3	brabga	$⊢ (A \in C \land B \in D) \to (A R B \leftrightarrow χ)$