Definition df-rel 4635

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5081 and dfrel3 5088. (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 4633	. 2 wff Rel A
3		cvv 2739	. . . 4 class _V
4	3, 3	cxp 4626	. . 3 class ( _V X. _V )
5	1, 4	wss 3131	. 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  4666  0nelrel  4674  releq  4710  nfrel  4713  sbcrel  4714  relss  4715  ssrel  4716  elrel  4730  relsng  4731  relsn  4733  relxp  4737  relun  4745  reliun  4749  reliin  4750  rel0  4753  relopabi  4754  relop  4779  eqbrrdva  4799  elreldm  4855  issref  5013  cnvcnv  5083  relrelss  5157  cnviinm  5172  nfunv  5251  funinsn  5267  oprabss  5963  1st2nd  6184  1stdm  6185  releldm2  6188  reldmtpos  6256  dmtpos  6259  dftpos4  6266  tpostpos  6267  iinerm  6609  fundmen  6808  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  reldvdsrsrg  13266  reldvg  14187