Definition df-rel 4605

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5048 and dfrel3 5055. (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 4603	. 2 wff Rel A
3		cvv 2721	. . . 4 class _V
4	3, 3	cxp 4596	. . 3 class ( _V X. _V )
5	1, 4	wss 3111	. 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  4636  0nelrel  4644  releq  4680  nfrel  4683  sbcrel  4684  relss  4685  ssrel  4686  elrel  4700  relsng  4701  relsn  4703  relxp  4707  relun  4715  reliun  4719  reliin  4720  rel0  4723  relopabi  4724  relop  4748  eqbrrdva  4768  elreldm  4824  issref  4980  cnvcnv  5050  relrelss  5124  cnviinm  5139  nfunv  5215  funinsn  5231  oprabss  5919  1st2nd  6141  1stdm  6142  releldm2  6145  reldmtpos  6212  dmtpos  6215  dftpos4  6222  tpostpos  6223  iinerm  6564  fundmen  6763  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  reldvg  13189