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

Metamath Proof Explorer

Definition df-funss

Description: Define the class of all function sets (but not necessarily function relations, cf. df-funsALTV ). It is used only by df-funsALTV . (Contributed by Peter Mazsa, 17-Jul-2021)

		Ref	Expression
	Assertion	df-funss	⊢ Funss = { 𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfunss	⊢ Funss
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3	2	ccoss	⊢ ≀ 𝑥
4		ccnvrefrels	⊢ CnvRefRels
5	3 4	wcel	⊢ ≀ 𝑥 ∈ CnvRefRels
6	5 1	cab	⊢ { 𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }
7	0 6	wceq	⊢ Funss = { 𝑥 ∣ ≀ 𝑥 ∈ CnvRefRels }