Definition df-rel 4730

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5185 and dfrel3 5192. (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 4728	. 2 wff Rel A
3		cvv 2800	. . . 4 class _V
4	3, 3	cxp 4721	. . 3 class ( _V X. _V )
5	1, 4	wss 3198	. 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  4762  0nelrel  4770  releq  4806  nfrel  4809  sbcrel  4810  relss  4811  ssrel  4812  elrel  4826  relsng  4827  relsn  4829  relxp  4833  relun  4842  reliun  4846  reliin  4847  rel0  4850  relopabiv  4851  relopabi  4853  relop  4878  eqbrrdva  4898  elreldm  4956  issref  5117  cnvcnv  5187  relrelss  5261  cnviinm  5276  nfunv  5357  funinsn  5376  oprabss  6102  relmptopab  6219  1st2nd  6339  1stdm  6340  releldm2  6343  reldmtpos  6414  dmtpos  6417  dftpos4  6424  tpostpos  6425  iinerm  6771  fundmen  6976  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  relelbasov  13135  reldvg  15393