Not directly but you can achieve many of the things you'd want to with
constructions like { x | ph } or with using a subset of { (/) } as a way
of representing a truth value.
Many of the examples I can think of are in iset.mm, for example
* https://us.metamath.org/ileuni/df-exmid.html
* https://us.metamath.org/ileuni/nndc.html
* https://us.metamath.org/ileuni/mkvprop.html
On 1/3/25 07:10, 'Peter Dolland' via Metamath wrote:
Is there any set of wffs?
Is there an equality (not equivalence) of wffs? So ` -. -. ph =/= ph ` .
Is a mapping of wffs into classes possible?
Clarification very appreciated!
Thank you!
Peter Dolland
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/4427844a-16b3-40c7-8b2f-d673460c1037%40panix.com.
