Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ax13w | Structured version Visualization version Unicode version |
Description: Weak version (principal instance) of ax-13 2246. (Because and don't need to be distinct, this actually bundles the principal instance and the degenerate instance .) Uses only Tarski's FOL axiom schemes. The proof is trivial but is included to complete the set ax10w 2006, ax11w 2007, and ax12w 2010. (Contributed by NM, 10-Apr-2017.) |
Ref | Expression |
---|---|
ax13w |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax5d 1840 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-5 1839 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |