Definition df-rel 4728

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

This definition is referenced by:  brrelex12  4760  0nelrel  4768  releq  4804  nfrel  4807  sbcrel  4808  relss  4809  ssrel  4810  elrel  4824  relsng  4825  relsn  4827  relxp  4831  relun  4840  reliun  4844  reliin  4845  rel0  4848  relopabiv  4849  relopabi  4851  relop  4876  eqbrrdva  4896  elreldm  4954  issref  5115  cnvcnv  5185  relrelss  5259  cnviinm  5274  nfunv  5355  funinsn  5374  oprabss  6100  relmptopab  6217  1st2nd  6337  1stdm  6338  releldm2  6341  reldmtpos  6412  dmtpos  6415  dftpos4  6422  tpostpos  6423  iinerm  6769  fundmen  6974  frecuzrdgtcl  10662  frecuzrdgfunlem  10669  relelbasov  13132  reldvg  15390