Description: Derive Axiom ax-hvmulid from Hilbert space under ZF set theory. (Contributed by NM, 31-May-2008) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | axhil.1 | ||
axhil.2 | |||
Assertion | axhvmulid-zf |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | axhil.1 | ||
2 | axhil.2 | ||
3 | df-hba | ||
4 | 1 | fveq2i | |
5 | 3 4 | eqtr4i | |
6 | 2 | hlnvi | |
7 | 1 6 | h2hsm | |
8 | 5 7 | hlmulid | |
9 | 2 8 | mpan |