Mathbox for Norm Megill < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax11wK Unicode version

Theorem ax11wK 27824
 Description: Weak version of ax-11 1624 from which we can prove any ax-7 1535 instance not involving wff variables or bundling. Uses only Tarski's predicate calculus axiom schemes i.e. does not use ax-6 1534, ax-7 1535, ax-11 1624, or ax-12 1633, and uses ax-9v 1632 instead of ax-9 1684. An instance of the first hypothesis will normally require that and be distinct (unless does not occur in ). See the description in the comment of equidK 27792. (Contributed by NM, 10-Apr-2017.)
Hypotheses
Ref Expression
ax11wK.1
ax11wK.2
Assertion
Ref Expression
ax11wK
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem ax11wK
StepHypRef Expression
1 ax11wK.2 . . 3
21ax4wK 27807 . 2
3 ax11wK.1 . . 3
43ax11wlemK 27823 . 2
52, 4syl5 30 1
 Colors of variables: wff set class Syntax hints:   wi 6   wb 178  wal 1532 This theorem is referenced by:  ax11wdemoK  27826 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536  ax-8 1623  ax-17 1628  ax-9v 1632 This theorem depends on definitions:  df-bi 179  df-an 362
 Copyright terms: Public domain W3C validator