Definition df-rel 4686

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

This definition is referenced by:  brrelex12  4717  0nelrel  4725  releq  4761  nfrel  4764  sbcrel  4765  relss  4766  ssrel  4767  elrel  4781  relsng  4782  relsn  4784  relxp  4788  relun  4796  reliun  4800  reliin  4801  rel0  4804  relopabiv  4805  relopabi  4807  relop  4832  eqbrrdva  4852  elreldm  4909  issref  5070  cnvcnv  5140  relrelss  5214  cnviinm  5229  nfunv  5309  funinsn  5328  oprabss  6038  1st2nd  6274  1stdm  6275  releldm2  6278  reldmtpos  6346  dmtpos  6349  dftpos4  6356  tpostpos  6357  iinerm  6701  fundmen  6905  frecuzrdgtcl  10564  frecuzrdgfunlem  10571  relelbasov  12938  reldvdsrsrg  13898  reldvg  15195