Definition df-rel 4738

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5194 and dfrel3 5201. (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 4736	. 2 wff Rel 𝐴
3		cvv 2803	. . . 4 class V
4	3, 3	cxp 4729	. . 3 class (V × V)
5	1, 4	wss 3201	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 105	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4770  0nelrel  4778  releq  4814  nfrel  4817  sbcrel  4818  relss  4819  ssrel  4820  elrel  4834  relsng  4835  relsn  4837  relxp  4841  relun  4850  reliun  4854  reliin  4855  rel0  4858  relopabiv  4859  relopabi  4861  relop  4886  eqbrrdva  4906  elreldm  4964  issref  5126  cnvcnv  5196  relrelss  5270  cnviinm  5285  nfunv  5366  funinsn  5386  oprabss  6117  relmptopab  6234  1st2nd  6353  1stdm  6354  releldm2  6357  reldmtpos  6462  dmtpos  6465  dftpos4  6472  tpostpos  6473  iinerm  6819  fundmen  7024  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  relelbasov  13225  reldvg  15490