Definition df-rel 4671

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5121 and dfrel3 5128. (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 4669	. 2 wff Rel A
3		cvv 2763	. . . 4 class _V
4	3, 3	cxp 4662	. . 3 class ( _V X. _V )
5	1, 4	wss 3157	. 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  4702  0nelrel  4710  releq  4746  nfrel  4749  sbcrel  4750  relss  4751  ssrel  4752  elrel  4766  relsng  4767  relsn  4769  relxp  4773  relun  4781  reliun  4785  reliin  4786  rel0  4789  relopabiv  4790  relopabi  4792  relop  4817  eqbrrdva  4837  elreldm  4893  issref  5053  cnvcnv  5123  relrelss  5197  cnviinm  5212  nfunv  5292  funinsn  5308  oprabss  6012  1st2nd  6248  1stdm  6249  releldm2  6252  reldmtpos  6320  dmtpos  6323  dftpos4  6330  tpostpos  6331  iinerm  6675  fundmen  6874  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  relelbasov  12765  reldvdsrsrg  13724  reldvg  14999