New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ax12w | Unicode version |
Description: Weak version (principal instance) of ax-12 1925. (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 ax6w 1717, ax7w 1718, and ax11w 1721. (Contributed by NM, 10-Apr-2017.) |
Ref | Expression |
---|---|
ax12w |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | a17d 1617 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wal 1540 |
This theorem was proved from axioms: ax-1 5 ax-mp 8 ax-17 1616 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |