Theorem pwvrel

Description: A set is a binary relation if and only if it belongs to the powerclass of the cartesian square of the universal class. (Contributed by Peter Mazsa, 14-Jun-2018) (Revised by BJ, 16-Dec-2023)

	Ref	Expression
Assertion	pwvrel	$$⊢A\in V\to \left(A\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{Rel}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elpwg	$$⊢A\in V\to \left(A\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}\right)$$
2		df-rel	$$⊢\mathrm{Rel}A\leftrightarrow A\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	bitr4di	$$⊢A\in V\to \left(A\in 𝒫\left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \mathrm{Rel}A\right)$$