Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > stdpc5 | GIF version |
Description: An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis Ⅎ𝑥𝜑 can be thought of as emulating "𝑥 is not free in 𝜑." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example 𝑥 would not (for us) be free in 𝑥 = 𝑥 by nfequid 1590. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
Ref | Expression |
---|---|
stdpc5.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
stdpc5 | ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdpc5.1 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
2 | 1 | 19.21 1475 | . 2 ⊢ (∀𝑥(𝜑 → 𝜓) ↔ (𝜑 → ∀𝑥𝜓)) |
3 | 2 | biimpi 113 | 1 ⊢ (∀𝑥(𝜑 → 𝜓) → (𝜑 → ∀𝑥𝜓)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 Ⅎwnf 1349 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-4 1400 ax-ial 1427 ax-i5r 1428 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: sbalyz 1875 ra5 2846 |
Copyright terms: Public domain | W3C validator |