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

Metamath Proof Explorer

Theorem brabidgaw

Description: The law of concretion for a binary relation. Special case of brabga . Version of brabidga with a disjoint variable condition, which does not require ax-13 . (Contributed by Peter Mazsa, 24-Nov-2018) (Revised by GG, 2-Apr-2024)

		Ref	Expression
	Hypothesis	brabidgaw.1	$⊢ R = \{⟨x, y⟩ \| φ\}$
	Assertion	brabidgaw	$⊢ x R y \leftrightarrow φ$

Proof

Step	Hyp	Ref	Expression
1		brabidgaw.1	$⊢ R = \{⟨x, y⟩ \| φ\}$
2	1	breqi	$⊢ x R y \leftrightarrow x \{⟨x, y⟩ \| φ\} y$
3		df-br	$⊢ x \{⟨x, y⟩ \| φ\} y \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\}$
4		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow φ$
5	2 3 4	3bitri	$⊢ x R y \leftrightarrow φ$