Definition df-rel 4690

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5142 and dfrel3 5149. (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 4688	. 2 wff Rel A
3		cvv 2773	. . . 4 class _V
4	3, 3	cxp 4681	. . 3 class ( _V X. _V )
5	1, 4	wss 3170	. 2 wff A C_ ( _V X. _V )
6	2, 5	wb 105	1 wff ( Rel A <-> A C_ ( _V X. _V ) )

This definition is referenced by:  brrelex12  4721  0nelrel  4729  releq  4765  nfrel  4768  sbcrel  4769  relss  4770  ssrel  4771  elrel  4785  relsng  4786  relsn  4788  relxp  4792  relun  4800  reliun  4804  reliin  4805  rel0  4808  relopabiv  4809  relopabi  4811  relop  4836  eqbrrdva  4856  elreldm  4913  issref  5074  cnvcnv  5144  relrelss  5218  cnviinm  5233  nfunv  5313  funinsn  5332  oprabss  6044  1st2nd  6280  1stdm  6281  releldm2  6284  reldmtpos  6352  dmtpos  6355  dftpos4  6362  tpostpos  6363  iinerm  6707  fundmen  6912  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  relelbasov  12969  reldvdsrsrg  13929  reldvg  15226