Definition df-rel 3180

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

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 3170	. 2 wff Rel A
3		cvv 1807	. . . 4 class V
4	3, 3	cxp 3163	. . 3 class (V X. V)
5	1, 4	wss 2043	. 2 wff A (_ (V X. V)
6	2, 5	wb 146	1 wff (Rel A <-> A (_ (V X. V))

This definition is referenced by:  brrelex 3202  releq 3238  hbrel 3240  relss 3241  ssrel 3242  elrel 3248  relsn 3249  relxp 3250  relun 3256  reluni 3260  relopab 3261  rel0 3267  relop 3270  elreldm 3333  relres 3379  cnvcnv 3478  nfunv 3538  funopg 3539  dff2 3808  oprabss 3997  1st2nd 4098  1stdm 4099  fundmen 4415  vcoprnelem 8149  vcex 8151  nvrel 8173  relded 10553  reldded 10554  relrded 10555  relcat 10574  reldcat 10575  relrcat 10576

Copyright terms: Public domain