Definition df-rel 4681

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5132 and dfrel3 5139. (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 4679	. 2 wff Rel A
3		cvv 2771	. . . 4 class _V
4	3, 3	cxp 4672	. . 3 class ( _V X. _V )
5	1, 4	wss 3165	. 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  4712  0nelrel  4720  releq  4756  nfrel  4759  sbcrel  4760  relss  4761  ssrel  4762  elrel  4776  relsng  4777  relsn  4779  relxp  4783  relun  4791  reliun  4795  reliin  4796  rel0  4799  relopabiv  4800  relopabi  4802  relop  4827  eqbrrdva  4847  elreldm  4903  issref  5064  cnvcnv  5134  relrelss  5208  cnviinm  5223  nfunv  5303  funinsn  5322  oprabss  6030  1st2nd  6266  1stdm  6267  releldm2  6270  reldmtpos  6338  dmtpos  6341  dftpos4  6348  tpostpos  6349  iinerm  6693  fundmen  6897  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  relelbasov  12836  reldvdsrsrg  13796  reldvg  15093