Definition df-rel 2425

Description: Define a relation. Definition 6.4(1) of [TakeutiZaring] p. 23. For an alternate definition, see dfrel2 2660.

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 2415	. 2 wff Rel A
3		cvv 1348	. . . 4 class V
4	3, 3	cxp 2408	. . 3 class (V X. V)
5	1, 4	wss 1487	. 2 wff A (_ (V X. V)
6	2, 5	wb 127	1 wff (Rel A <-> A (_ (V X. V))

This definition is referenced by:  brrelex 2446  releq 2477  hbrel 2478  ssrel 2479  relss 2480  relsn 2485  relxp 2486  relun 2490  reluni 2493  relopab 2494  rel0 2499  elreldm 2554  relres 2591  imasn 2616  cnvcnv 2661  nfunv 2693  fundmen 3333

metamath.org