Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax10o  Unicode version 
Description: Axiom ax10o 2215 ("o" for "old") was the
original version of ax10 2216,
before it was discovered (in May 2008) that the shorter ax10 2216 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is obsolete and should no longer be used. It is proved above as theorem ax10o 2038. (Contributed by NM, 5Aug1993.) (New usage is discouraged.) 
Ref  Expression 

ax10o 
Step  Hyp  Ref  Expression 

1  vx  . . . 4  
2  vy  . . . 4  
3  1, 2  weq 1653  . . 3 
4  3, 1  wal 1549  . 2 
5  wph  . . . 4  
6  5, 1  wal 1549  . . 3 
7  5, 2  wal 1549  . . 3 
8  6, 7  wi 4  . 2 
9  4, 8  wi 4  1 
Colors of variables: wff set class 
This axiom is referenced by: aecomo 2227 hbaeo 2229 dral1o 2230 ax10from10o 2253 dvelimfo 2256 
Copyright terms: Public domain  W3C validator 