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 }