Theorem brabidga

Description: The law of concretion for a binary relation. Special case of brabga . Usage of this theorem is discouraged because it depends on ax-13 , see brabidgaw for a weaker version that does not require it. (Contributed by Peter Mazsa, 24-Nov-2018) (New usage is discouraged.)

	Ref	Expression
Hypothesis	brabidga.1	$$⊢R=\left\{⟨x,y⟩|\phi \right\}$$
Assertion	brabidga	$$⊢xRy\leftrightarrow \phi$$

Proof

Step	Hyp	Ref	Expression
1		brabidga.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		opabid	$$⊢⟨x,y⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \phi$$
5	2 3 4	3bitri	$$⊢xRy\leftrightarrow \phi$$