Definition df-rel 4420

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

This definition is referenced by:  brrelex12  4449  releq  4490  nfrel  4493  sbcrel  4494  relss  4495  ssrel  4496  elrel  4510  relsng  4511  relsn  4513  relxp  4517  relun  4524  reliun  4528  reliin  4529  rel0  4532  relopabi  4533  relop  4556  eqbrrdva  4576  elreldm  4631  issref  4783  cnvcnv  4851  relrelss  4925  cnviinm  4940  nfunv  5014  funinsn  5030  oprabss  5693  1st2nd  5910  1stdm  5911  releldm2  5914  reldmtpos  5974  dmtpos  5977  dftpos4  5984  tpostpos  5985  iinerm  6318  fundmen  6477  frecuzrdgtcl  9750  frecuzrdgfunlem  9757