Definition df-rel 4352

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4771 and dfrel3 4778. (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 4350	. 2 wff Rel 𝐴
3		cvv 2557	. . . 4 class V
4	3, 3	cxp 4343	. . 3 class (V × V)
5	1, 4	wss 2917	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 98	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4381  releq  4422  nfrel  4425  sbcrel  4426  relss  4427  ssrel  4428  elrel  4442  relsn  4443  relxp  4447  relun  4454  reliun  4458  reliin  4459  rel0  4462  relopabi  4463  relop  4486  eqbrrdva  4505  elreldm  4560  issref  4707  cnvcnv  4773  relrelss  4844  cnviinm  4859  nfunv  4933  oprabss  5590  1st2nd  5807  1stdm  5808  releldm2  5811  reldmtpos  5868  dmtpos  5871  dftpos4  5878  tpostpos  5879  iinerm  6178  fundmen  6286  frecuzrdgfn  9198