Definition df-rel 4651

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5097 and dfrel3 5104. (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 4649	. 2 wff Rel A
3		cvv 2752	. . . 4 class _V
4	3, 3	cxp 4642	. . 3 class ( _V X. _V )
5	1, 4	wss 3144	. 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  4682  0nelrel  4690  releq  4726  nfrel  4729  sbcrel  4730  relss  4731  ssrel  4732  elrel  4746  relsng  4747  relsn  4749  relxp  4753  relun  4761  reliun  4765  reliin  4766  rel0  4769  relopabi  4770  relop  4795  eqbrrdva  4815  elreldm  4871  issref  5029  cnvcnv  5099  relrelss  5173  cnviinm  5188  nfunv  5268  funinsn  5284  oprabss  5982  1st2nd  6206  1stdm  6207  releldm2  6210  reldmtpos  6278  dmtpos  6281  dftpos4  6288  tpostpos  6289  iinerm  6633  fundmen  6832  frecuzrdgtcl  10443  frecuzrdgfunlem  10450  relelbasov  12574  reldvdsrsrg  13442  reldvg  14605