Definition df-rel 4618

Description: Define the relation predicate. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 5061 and dfrel3 5068. (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 4616	. 2 wff Rel A
3		cvv 2730	. . . 4 class _V
4	3, 3	cxp 4609	. . 3 class ( _V X. _V )
5	1, 4	wss 3121	. 2 wff A C_ ( _V X. _V )
6	2, 5	wb 104	1 wff ( Rel A <-> A C_ ( _V X. _V ) )

This definition is referenced by:  brrelex12  4649  0nelrel  4657  releq  4693  nfrel  4696  sbcrel  4697  relss  4698  ssrel  4699  elrel  4713  relsng  4714  relsn  4716  relxp  4720  relun  4728  reliun  4732  reliin  4733  rel0  4736  relopabi  4737  relop  4761  eqbrrdva  4781  elreldm  4837  issref  4993  cnvcnv  5063  relrelss  5137  cnviinm  5152  nfunv  5231  funinsn  5247  oprabss  5939  1st2nd  6160  1stdm  6161  releldm2  6164  reldmtpos  6232  dmtpos  6235  dftpos4  6242  tpostpos  6243  iinerm  6585  fundmen  6784  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  reldvg  13442