Definition df-rel 4627

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

This definition is referenced by:  brrelex12  4658  0nelrel  4666  releq  4702  nfrel  4705  sbcrel  4706  relss  4707  ssrel  4708  elrel  4722  relsng  4723  relsn  4725  relxp  4729  relun  4737  reliun  4741  reliin  4742  rel0  4745  relopabi  4746  relop  4770  eqbrrdva  4790  elreldm  4846  issref  5003  cnvcnv  5073  relrelss  5147  cnviinm  5162  nfunv  5241  funinsn  5257  oprabss  5951  1st2nd  6172  1stdm  6173  releldm2  6176  reldmtpos  6244  dmtpos  6247  dftpos4  6254  tpostpos  6255  iinerm  6597  fundmen  6796  frecuzrdgtcl  10380  frecuzrdgfunlem  10387  reldvg  13699