Definition df-rel 4725

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5178 and dfrel3 5185. (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 4723	. 2 wff Rel A
3		cvv 2799	. . . 4 class _V
4	3, 3	cxp 4716	. . 3 class ( _V X. _V )
5	1, 4	wss 3197	. 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  4756  0nelrel  4764  releq  4800  nfrel  4803  sbcrel  4804  relss  4805  ssrel  4806  elrel  4820  relsng  4821  relsn  4823  relxp  4827  relun  4835  reliun  4839  reliin  4840  rel0  4843  relopabiv  4844  relopabi  4846  relop  4871  eqbrrdva  4891  elreldm  4949  issref  5110  cnvcnv  5180  relrelss  5254  cnviinm  5269  nfunv  5350  funinsn  5369  oprabss  6089  1st2nd  6325  1stdm  6326  releldm2  6329  reldmtpos  6397  dmtpos  6400  dftpos4  6407  tpostpos  6408  iinerm  6752  fundmen  6957  frecuzrdgtcl  10629  frecuzrdgfunlem  10636  relelbasov  13090  reldvdsrsrg  14050  reldvg  15347