Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax10o  Unicode version 
Description: Axiom ax10o 2189 ("o" for "old") was the
original version of ax10 2190,
before it was discovered (in May 2008) that the shorter ax10 2190 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 2201 hbaeo 2203 dral1o 2204 ax10from10o 2227 dvelimfo 2230 
Copyright terms: Public domain  W3C validator 