MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-5o Unicode version

Axiom ax-5o 2075
Description: Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying  ps. Notice that  x must not be a free variable in the antecedent of the quantified implication, and we express this by binding  ph to "protect" the axiom from a  ph containing a free  x. 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 1717. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Assertion
Ref Expression
ax-5o  |-  ( A. x ( A. x ph  ->  ps )  -> 
( A. x ph  ->  A. x ps )
)

Detailed syntax breakdown of Axiom ax-5o
StepHypRef Expression
1 wph . . . . 5  wff  ph
2 vx . . . . 5  set  x
31, 2wal 1527 . . . 4  wff  A. x ph
4 wps . . . 4  wff  ps
53, 4wi 4 . . 3  wff  ( A. x ph  ->  ps )
65, 2wal 1527 . 2  wff  A. x
( A. x ph  ->  ps )
74, 2wal 1527 . . 3  wff  A. x ps
83, 7wi 4 . 2  wff  ( A. x ph  ->  A. x ps )
96, 8wi 4 1  wff  ( A. x ( A. x ph  ->  ps )  -> 
( A. x ph  ->  A. x ps )
)
Colors of variables: wff set class
This axiom is referenced by:  ax5  2085  ax6  2086  equid1  2097
  Copyright terms: Public domain W3C validator