Definition df-rel 3175

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

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 3165	. 2 wff Rel A
3		cvv 1802	. . . 4 class V
4	3, 3	cxp 3158	. . 3 class (V X. V)
5	1, 4	wss 2037	. 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 3197  releq 3233  hbrel 3235  relss 3236  ssrel 3237  elrel 3243  relsn 3244  relxp 3245  relun 3251  reluni 3255  relopab 3256  rel0 3262  relop 3265  elreldm 3327  relres 3371  cnvcnv 3472  nfunv 3532  funopg 3533  dff2 3802  oprabss 3991  1st2nd 4092  1stdm 4093  fundmen 4409  vcoprnelem 8135  vcex 8137  nvrel 8159  relded 10517  reldded 10518  relrded 10519  relcat 10538  reldcat 10539  relrcat 10540

Copyright terms: Public domain