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	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wrel	⊢ Rel 𝐴
2		cvv	⊢ V
3	2 2	cxp	⊢ ( V × V )
4	0 3	wss	⊢ 𝐴 ⊆ ( V × V )
5	1 4	wb	⊢ ( Rel 𝐴 ↔ 𝐴 ⊆ ( V × V ) )