Definition df-rel 4633

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

This definition is referenced by:  brrelex12  4664  0nelrel  4672  releq  4708  nfrel  4711  sbcrel  4712  relss  4713  ssrel  4714  elrel  4728  relsng  4729  relsn  4731  relxp  4735  relun  4743  reliun  4747  reliin  4748  rel0  4751  relopabi  4752  relop  4777  eqbrrdva  4797  elreldm  4853  issref  5011  cnvcnv  5081  relrelss  5155  cnviinm  5170  nfunv  5249  funinsn  5265  oprabss  5960  1st2nd  6181  1stdm  6182  releldm2  6185  reldmtpos  6253  dmtpos  6256  dftpos4  6263  tpostpos  6264  iinerm  6606  fundmen  6805  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  reldvdsrsrg  13259  reldvg  14118