Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax10o  Unicode version 
Description: Axiom ax10o 2187 ("o" for "old") was the
original version of ax10 2188,
before it was discovered (in May 2008) that the shorter ax10 2188 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 2001. (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 1650  . . 3 
4  3, 1  wal 1546  . 2 
5  wph  . . . 4  
6  5, 1  wal 1546  . . 3 
7  5, 2  wal 1546  . . 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 2199 hbaeo 2201 dral1o 2202 ax10from10o 2225 dvelimfo 2228 
Copyright terms: Public domain  W3C validator 