Users' Mathboxes Mathbox for Peter Mazsa < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-funsALTV Structured version   Visualization version   GIF version

Definition df-funsALTV 39838
Description: Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV 39840, ... , dffunsALTV5 39844. (Contributed by Peter Mazsa, 17-Jul-2021.)
Assertion
Ref Expression
df-funsALTV FunsALTV = ( Funss ∩ Rels )

Detailed syntax breakdown of Definition df-funsALTV
StepHypRef Expression
1 cfunsALTV 39287 . 2 class FunsALTV
2 cfunss 39286 . . 3 class Funss
3 crels 39257 . . 3 class Rels
42, 3cin 4091 . 2 class ( Funss ∩ Rels )
51, 4wceq 1569 1 wff FunsALTV = ( Funss ∩ Rels )
Colors of variables:    wff setvar class
This definition is used by:  dffunsALTV  39840
  Copyright terms: Public domain W3C validator