Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > axi12  Structured version Unicode version 
Description: Axiom of Quantifier
Introduction. One of the equality and substitution
axioms of predicate calculus with equality. Informally, it says that
whenever is
distinct from and
, and
is true,
then quantified with is also true. In other words,
is irrelevant to the truth of
. Axiom scheme C9' in
[Megill]
p. 448 (p. 16 of the preprint). It apparently does not otherwise appear
in the literature but is easily proved from textbook predicate calculus by
cases.
This axiom has been modified from the original ax12 1378 for compatibility with intuitionistic logic. (Contributed by Mario Carneiro, 31Jan2015.) 
Ref  Expression 

axi12 
Step  Hyp  Ref  Expression 

1  vz  . . . 4  
2  vx  . . . 4  
3  1, 2  weq 1368  . . 3 
4  3, 1  wal 1224  . 2 
5  vy  . . . . 5  
6  1, 5  weq 1368  . . . 4 
7  6, 1  wal 1224  . . 3 
8  2, 5  weq 1368  . . . . 5 
9  8, 1  wal 1224  . . . . 5 
10  8, 9  wi 4  . . . 4 
11  10, 1  wal 1224  . . 3 
12  7, 11  wo 613  . 2 
13  4, 12  wo 613  1 
Colors of variables: wff set class 
This axiom is referenced by: ax12 1378 ax12or 1379 dveeq2 1672 dveeq2or 1673 dvelimALT 1862 dvelimfv 1863 
Copyright terms: Public domain  W3C validator 