Definition df-rel 4671

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

This definition is referenced by:  brrelex12  4702  0nelrel  4710  releq  4746  nfrel  4749  sbcrel  4750  relss  4751  ssrel  4752  elrel  4766  relsng  4767  relsn  4769  relxp  4773  relun  4781  reliun  4785  reliin  4786  rel0  4789  relopabiv  4790  relopabi  4792  relop  4817  eqbrrdva  4837  elreldm  4893  issref  5053  cnvcnv  5123  relrelss  5197  cnviinm  5212  nfunv  5292  funinsn  5308  oprabss  6009  1st2nd  6240  1stdm  6241  releldm2  6244  reldmtpos  6312  dmtpos  6315  dftpos4  6322  tpostpos  6323  iinerm  6667  fundmen  6866  frecuzrdgtcl  10506  frecuzrdgfunlem  10513  relelbasov  12750  reldvdsrsrg  13658  reldvg  14925