Definition df-rel 4666

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5116 and dfrel3 5123. (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 4664	. 2 wff Rel A
3		cvv 2760	. . . 4 class _V
4	3, 3	cxp 4657	. . 3 class ( _V X. _V )
5	1, 4	wss 3153	. 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  4697  0nelrel  4705  releq  4741  nfrel  4744  sbcrel  4745  relss  4746  ssrel  4747  elrel  4761  relsng  4762  relsn  4764  relxp  4768  relun  4776  reliun  4780  reliin  4781  rel0  4784  relopabiv  4785  relopabi  4787  relop  4812  eqbrrdva  4832  elreldm  4888  issref  5048  cnvcnv  5118  relrelss  5192  cnviinm  5207  nfunv  5287  funinsn  5303  oprabss  6004  1st2nd  6234  1stdm  6235  releldm2  6238  reldmtpos  6306  dmtpos  6309  dftpos4  6316  tpostpos  6317  iinerm  6661  fundmen  6860  frecuzrdgtcl  10483  frecuzrdgfunlem  10490  relelbasov  12680  reldvdsrsrg  13588  reldvg  14833