Theorem dfrel4

Description: A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 for relations. (Contributed by Mario Carneiro, 16-Aug-2015) (Revised by Thierry Arnoux, 11-May-2017)

	Ref	Expression
Hypotheses	dfrel4.1	$$⊢\underset{\_}{Ⅎ}xR$$
	dfrel4.2	$$⊢\underset{\_}{Ⅎ}yR$$
Assertion	dfrel4	$$⊢\mathrm{Rel}R\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dfrel4.1	$$⊢\underset{\_}{Ⅎ}xR$$
2		dfrel4.2	$$⊢\underset{\_}{Ⅎ}yR$$
3		dfrel4v	$$⊢\mathrm{Rel}R\leftrightarrow R=\left\{⟨a,b⟩|aRb\right\}$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xa$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xb$$
6	4 1 5	nfbr	$$⊢ℲxaRb$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}ya$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}yb$$
9	7 2 8	nfbr	$$⊢ℲyaRb$$
10		nfv	$$⊢ℲaxRy$$
11		nfv	$$⊢ℲbxRy$$
12		breq12	$$⊢\left(a=x\wedge b=y\right)\to \left(aRb\leftrightarrow xRy\right)$$
13	6 9 10 11 12	cbvopab	$$⊢\left\{⟨a,b⟩|aRb\right\}=\left\{⟨x,y⟩|xRy\right\}$$
14	13	eqeq2i	$$⊢R=\left\{⟨a,b⟩|aRb\right\}\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$
15	3 14	bitri	$$⊢\mathrm{Rel}R\leftrightarrow R=\left\{⟨x,y⟩|xRy\right\}$$