Definition df-rel 4611

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5054 and dfrel3 5061. (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 4609	. 2 wff Rel 𝐴
3		cvv 2726	. . . 4 class V
4	3, 3	cxp 4602	. . 3 class (V × V)
5	1, 4	wss 3116	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 104	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4642  0nelrel  4650  releq  4686  nfrel  4689  sbcrel  4690  relss  4691  ssrel  4692  elrel  4706  relsng  4707  relsn  4709  relxp  4713  relun  4721  reliun  4725  reliin  4726  rel0  4729  relopabi  4730  relop  4754  eqbrrdva  4774  elreldm  4830  issref  4986  cnvcnv  5056  relrelss  5130  cnviinm  5145  nfunv  5221  funinsn  5237  oprabss  5928  1st2nd  6149  1stdm  6150  releldm2  6153  reldmtpos  6221  dmtpos  6224  dftpos4  6231  tpostpos  6232  iinerm  6573  fundmen  6772  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  reldvg  13288