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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 ( V × V ) ↔ Rel 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elpwg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 ( V × V ) ↔ 𝐴 ⊆ ( V × V ) ) )
2		df-rel	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )
3	1 2	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ 𝒫 ( V × V ) ↔ Rel 𝐴 ) )