Description: Special case of Theorem
19.21 of [Margaris] p. 90. Notational
convention: We sometimes suffix with "v" the label of a
theorem
eliminating a hypothesis such as ![( (](lp.gif)
![A. A.](forall.gif) ![x x](_x.gif) ![ph ph](_varphi.gif) in
19.21 1563 via
the use of distinct variable conditions combined with ax-17 1507.
Conversely, we sometimes suffix with "f" the label of a
theorem
introducing such a hypothesis to eliminate the need for the distinct
variable condition; e.g., euf 2005 derived from df-eu 2003. The "f" stands
for "not free in" which is less restrictive than "does
not occur in".
(Contributed by NM, 5-Aug-1993.) |