Definition df-rel 4783

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5241 and dfrel3 5248. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-rel	|- ( Rel A <-> A C_ ( _V X. _V ) )

Detailed syntax breakdown of Definition df-rel

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wrel 4781	. 2 wff Rel A
3		cvv 2821	. . . 4 class _V
4	3, 3	cxp 4774	. . 3 class ( _V X. _V )
5	1, 4	wss 3220	. 2 wff A C_ ( _V X. _V )
6	2, 5	wb 105	1 wff ( Rel A <-> A C_ ( _V X. _V ) )

This definition is used by:  brrelex12  4815  0nelrel  4823  releq  4859  nfrel  4862  sbcrel  4863  relss  4864  ssrel  4865  elrel  4879  relsng  4880  relsn  4882  relxp  4886  relun  4896  reliun  4900  reliin  4901  rel0  4904  relopabiv  4905  relopabi  4907  relop  4932  eqbrrdva  4952  elreldm  5010  issref  5173  cnvcnv  5243  relrelss  5317  cnviinm  5332  nfunv  5413  funinsn  5433  oprabss  6177  relmptopab  6294  1st2nd  6419  1stdm  6420  releldm2  6423  reldmtpos  6528  dmtpos  6531  dftpos4  6538  tpostpos  6539  iinerm  6885  fundmen  7098  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  relelbasov  13474  reldvg  15905