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=\left\{⟨x,y⟩|\phi \right\}$$
Assertion	brabidgaw	$$⊢xRy\leftrightarrow \phi$$

Proof

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