Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > ax12w  Unicode version 
Description: Weak version (principal instance) of ax12 1946. (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 1728, ax7w 1729, and ax11w 1732. (Contributed by NM, 10Apr2017.) 
Ref  Expression 

ax12w 
Step  Hyp  Ref  Expression 

1  a17d 1624  1 
Colors of variables: wff set class 
Syntax hints: wn 3 wi 4 wal 1546 
This theorem was proved from axioms: ax1 5 axmp 8 ax17 1623 
Copyright terms: Public domain  W3C validator 