Definition df-rel 4370

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4791 and dfrel3 4798. (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 4368	. 2 wff Rel 𝐴
3		cvv 2601	. . . 4 class V
4	3, 3	cxp 4361	. . 3 class (V × V)
5	1, 4	wss 2973	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 103	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4399  releq  4440  nfrel  4443  sbcrel  4444  relss  4445  ssrel  4446  elrel  4460  relsn  4461  relxp  4465  relun  4472  reliun  4476  reliin  4477  rel0  4480  relopabi  4481  relop  4504  eqbrrdva  4523  elreldm  4578  issref  4727  cnvcnv  4793  relrelss  4864  cnviinm  4879  nfunv  4953  oprabss  5610  1st2nd  5827  1stdm  5828  releldm2  5831  reldmtpos  5891  dmtpos  5894  dftpos4  5901  tpostpos  5902  iinerm  6201  fundmen  6309  frecuzrdgfn  9414