This has been bugging me midly for a while, but I couldn't figure out what the
Fr symbol in df-fr stood for:
19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x
A. z e. x -. z R y ) ) $.
I finally bothered to look up the Takeuti and Zaring reference, which also uses
"Fr" and calls R a "foundational relation". It's not super important, but would
it be worth mentioning this in df-fr's comment?
Cheers,
B. Wilson
--
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 on the web visit
https://groups.google.com/d/msgid/metamath/2F5KIFFJJY2KH.28Z6N87TP90O2%40wilsonb.com.
