Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax10o  Unicode version 
Description: Axiom ax10o 2173 ("o" for "old") was the
original version of ax10 2174,
before it was discovered (in May 2008) that the shorter ax10 2174 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 1991. (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 2185 hbaeo 2187 dral1o 2188 ax10from10o 2211 dvelimfo 2214 
Copyright terms: Public domain  W3C validator 