brismu bridi		< Previous   Next > Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ax-dgen1

---

Axiom ax-dgen1 444

Description: Special case of first-order generalization where the quantified variable does not occur in the bridi.

Assertion

Ref	Expression
ax-dgen1	⊢ ganai broda gi ro da zo'u broda

Distinct variable group:   broda , da

---

This axiom is referenced by:  nfv  445

Copyright terms: Public domain

W3C validator