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

Axiom ax-c4 2215
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 . 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 axc4 1860. (Contributed by NM, 3-Jan-1993.) (New usage is discouraged.)

Assertion
Ref Expression
ax-c4

Detailed syntax breakdown of Axiom ax-c4
StepHypRef Expression
1 wph . . . . 5
2 vx . . . . 5
31, 2wal 1393 . . . 4
4 wps . . . 4
53, 4wi 4 . . 3
65, 2wal 1393 . 2
74, 2wal 1393 . . 3
83, 7wi 4 . 2
96, 8wi 4 1
Colors of variables: wff setvar class
This axiom is referenced by:  ax4  2225  ax10  2226  equid1  2237
  Copyright terms: Public domain W3C validator