NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax-5o Unicode version

Axiom ax-5o 2136
Description: Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying . Notice that must not be a free variable in the antecedent of the quantified implication, and we express this by binding to "protect" the axiom from a containing a free . One of the 4 axioms of "pure" predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.

This axiom is obsolete and should no longer be used. It is proved above as theorem ax5o 1749. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Assertion
Ref Expression
ax-5o

Detailed syntax breakdown of Axiom ax-5o
StepHypRef Expression
1 wph . . . . 5
2 vx . . . . 5
31, 2wal 1540 . . . 4
4 wps . . . 4
53, 4wi 4 . . 3
65, 2wal 1540 . 2
74, 2wal 1540 . . 3
83, 7wi 4 . 2
96, 8wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  ax5  2146  ax6  2147  equid1  2158
  Copyright terms: Public domain W3C validator