Definition df-rel

Description: Define the relation predicate. Definition 6.4(1) of TakeutiZaring p. 23. For alternate definitions, see dfrel2 and dfrel3 . (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Assertion	df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wrel	$$wff\mathrm{Rel}A$$
2		cvv	$$class\mathrm{V}$$
3	2 2	cxp	$$class\left(\mathrm{V}\times \mathrm{V}\right)$$
4	0 3	wss	$$wffA\subseteq \mathrm{V}\times \mathrm{V}$$
5	1 4	wb	$$wff\left(\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}\right)$$