This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-funsALTV

Description: Define the function relations class, i.e., the class of functions. Alternate definitions are dffunsALTV , ... , dffunsALTV5 . (Contributed by Peter Mazsa, 17-Jul-2021)

		Ref	Expression
	Assertion	df-funsALTV	$⊢ FunsALTV = Funss \cap Rels$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunsALTV	$class FunsALTV$
1		cfunss	$class Funss$
2		crels	$class Rels$
3	1 2	cin	$class (Funss \cap Rels)$
4	0 3	wceq	$wff FunsALTV = Funss \cap Rels$