Definition df-rel 3266

Description: Define a relation. Definition 6.4(1) of [TakeutiZaring] p. 23. For alternate definitions, see dfrel2 3569 and dfrel3 3587.

Assertion

Ref	Expression
df-rel	|- (Rel A <-> A (_ (V X. V))

Detailed syntax breakdown of Definition df-rel

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	wrel 3256	. 2 wff Rel A
3		cvv 1857	. . . 4 class V
4	3, 3	cxp 3249	. . 3 class (V X. V)
5	1, 4	wss 2099	. 2 wff A (_ (V X. V)
6	2, 5	wb 144	1 wff (Rel A <-> A (_ (V X. V))

This definition is referenced by:  brrelex 3290  releq 3330  hbrel 3332  relss 3333  ssrel 3334  elrel 3342  relsn 3343  relxp 3344  relun 3350  reliun 3354  rel0 3355  relopab 3357  relop 3365  elreldm 3425  relres 3477  cnvcnv 3570  relrelss 3618  nfunv 3651  funopg 3652  dff3 3931  oprabss 4066  1st2nd 4168  1stdm 4169  fundmen 4569  vcoprnelem 8444  vcex 8446  nvrel 8468  ref3w 10772  prj1 10809  prj1b 10811  relded 11194  reldded 11195  relrded 11196  relcat 11215  reldcat 11216  relrcat 11217

Copyright terms: Public domain