Definition df-rel 4783

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

Assertion

Ref	Expression
df-rel	⊢ (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

Detailed syntax breakdown of Definition df-rel

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wrel 4781	. 2 wff Rel 𝐴
3		cvv 2821	. . . 4 class V
4	3, 3	cxp 4774	. . 3 class (V × V)
5	1, 4	wss 3220	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 105	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is used by:  brrelex12  4815  0nelrel  4823  releq  4859  nfrel  4862  sbcrel  4863  relss  4864  ssrel  4865  elrel  4879  relsng  4880  relsn  4882  relxp  4886  relun  4896  reliun  4900  reliin  4901  rel0  4904  relopabiv  4905  relopabi  4907  relop  4932  eqbrrdva  4952  elreldm  5010  issref  5173  cnvcnv  5243  relrelss  5317  cnviinm  5332  nfunv  5413  funinsn  5433  oprabss  6177  relmptopab  6294  1st2nd  6419  1stdm  6420  releldm2  6423  reldmtpos  6529  dmtpos  6532  dftpos4  6539  tpostpos  6540  iinerm  6886  fundmen  7100  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  relelbasov  13473  reldvg  15922