NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-fix Unicode version

Definition df-fix 5740
Description: Define the fixed points of a relationship. (Contributed by SF, 9-Feb-2015.)
Assertion
Ref Expression
df-fix

Detailed syntax breakdown of Definition df-fix
StepHypRef Expression
1 cA . . 3
21cfix 5739 . 2
3 cid 4763 . . . 4
41, 3cin 3208 . . 3
54crn 4773 . 2
62, 5wceq 1642 1
Colors of variables: wff setvar class
This definition is referenced by:  elfix  5787  fixexg  5788
  Copyright terms: Public domain W3C validator