NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  ax12w Unicode version

Theorem ax12w 1724
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
Distinct variable groups:   ,   ,

Proof of Theorem ax12w
StepHypRef 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