Definition df-rel 4554

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4997 and dfrel3 5004. (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 4552	. 2 wff Rel 𝐴
3		cvv 2689	. . . 4 class V
4	3, 3	cxp 4545	. . 3 class (V × V)
5	1, 4	wss 3076	. 2 wff 𝐴 ⊆ (V × V)
6	2, 5	wb 104	1 wff (Rel 𝐴 ↔ 𝐴 ⊆ (V × V))

This definition is referenced by:  brrelex12  4585  0nelrel  4593  releq  4629  nfrel  4632  sbcrel  4633  relss  4634  ssrel  4635  elrel  4649  relsng  4650  relsn  4652  relxp  4656  relun  4664  reliun  4668  reliin  4669  rel0  4672  relopabi  4673  relop  4697  eqbrrdva  4717  elreldm  4773  issref  4929  cnvcnv  4999  relrelss  5073  cnviinm  5088  nfunv  5164  funinsn  5180  oprabss  5865  1st2nd  6087  1stdm  6088  releldm2  6091  reldmtpos  6158  dmtpos  6161  dftpos4  6168  tpostpos  6169  iinerm  6509  fundmen  6708  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  reldvg  12856