Definition df-rel 4408

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4835 and dfrel3 4842. (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 4406	. 2 wff Rel A
3		cvv 2612	. . . 4 class _V
4	3, 3	cxp 4399	. . 3 class ( _V X. _V )
5	1, 4	wss 2984	. 2 wff A C_ ( _V X. _V )
6	2, 5	wb 103	1 wff ( Rel A <-> A C_ ( _V X. _V ) )

This definition is referenced by:  brrelex12  4437  releq  4478  nfrel  4481  sbcrel  4482  relss  4483  ssrel  4484  elrel  4498  relsng  4499  relsn  4501  relxp  4505  relun  4512  reliun  4516  reliin  4517  rel0  4520  relopabi  4521  relop  4544  eqbrrdva  4564  elreldm  4619  issref  4769  cnvcnv  4837  relrelss  4911  cnviinm  4926  nfunv  5000  funinsn  5016  oprabss  5669  1st2nd  5886  1stdm  5887  releldm2  5890  reldmtpos  5950  dmtpos  5953  dftpos4  5960  tpostpos  5961  iinerm  6294  fundmen  6453  frecuzrdgtcl  9708  frecuzrdgfunlem  9715