Definition df-rel 3185

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

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 3175	. 2 wff Rel A
3		cvv 1811	. . . 4 class V
4	3, 3	cxp 3168	. . 3 class (V X. V)
5	1, 4	wss 2047	. 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 3207  releq 3243  hbrel 3245  relss 3246  ssrel 3247  elrel 3253  relsn 3254  relxp 3255  relun 3261  reluni 3265  relopab 3266  rel0 3272  relop 3275  elreldm 3338  relres 3387  cnvcnv 3486  nfunv 3546  funopg 3547  dff2 3817  oprabss 4006  1st2nd 4108  1stdm 4109  fundmen 4428  vcoprnelem 8197  vcex 8199  nvrel 8221  relded 10673  reldded 10674  relrded 10675  relcat 10694  reldcat 10695  relrcat 10696

Copyright terms: Public domain