Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax12o  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 is obsolete and should no longer be used. It is proved above as theorem ax12o 1976. (Contributed by NM, 5Aug1993.) (New usage is discouraged.) 
Ref  Expression 

ax12o 
Step  Hyp  Ref  Expression 

1  vz  . . . . 5  
2  vx  . . . . 5  
3  1, 2  weq 1650  . . . 4 
4  3, 1  wal 1546  . . 3 
5  4  wn 3  . 2 
6  vy  . . . . . 6  
7  1, 6  weq 1650  . . . . 5 
8  7, 1  wal 1546  . . . 4 
9  8  wn 3  . . 3 
10  2, 6  weq 1650  . . . 4 
11  10, 1  wal 1546  . . . 4 
12  10, 11  wi 4  . . 3 
13  9, 12  wi 4  . 2 
14  5, 13  wi 4  1 
Colors of variables: wff set class 
This axiom is referenced by: hbaeo 2201 ax12from12o 2204 equid1 2206 hbequid 2208 equid1ALT 2224 dvelimfo 2228 ax17eq 2231 
Copyright terms: Public domain  W3C validator 