Definition df-rel 4484

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 4925 and dfrel3 4932. (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 4482	. 2 wff Rel A
3		cvv 2641	. . . 4 class _V
4	3, 3	cxp 4475	. . 3 class ( _V X. _V )
5	1, 4	wss 3021	. 2 wff A C_ ( _V X. _V )
6	2, 5	wb 104	1 wff ( Rel A <-> A C_ ( _V X. _V ) )

This definition is referenced by:  brrelex12  4515  0nelrel  4523  releq  4559  nfrel  4562  sbcrel  4563  relss  4564  ssrel  4565  elrel  4579  relsng  4580  relsn  4582  relxp  4586  relun  4594  reliun  4598  reliin  4599  rel0  4602  relopabi  4603  relop  4627  eqbrrdva  4647  elreldm  4703  issref  4857  cnvcnv  4927  relrelss  5001  cnviinm  5016  nfunv  5092  funinsn  5108  oprabss  5789  1st2nd  6009  1stdm  6010  releldm2  6013  reldmtpos  6080  dmtpos  6083  dftpos4  6090  tpostpos  6091  iinerm  6431  fundmen  6630  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  reldvg  12521