Metamath Proof Explorer

Table of Contents - 21.5.1. First-order logic

1. Auxiliary axiom schemes
   1. nfan1c
   2. cbvex1v
   3. dvelimalcased
   4. dvelimalcasei
   5. dvelimexcased
   6. dvelimexcasei