Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax11w Unicode version

Theorem ax11w 1707
 Description: Weak version of ax-11 1727 from which we can prove any ax-11 1727 instance not involving wff variables or bundling. Uses only Tarski's FOL axiom schemes. An instance of the first hypothesis will normally require that and be distinct (unless does not occur in ). (Contributed by NM, 10-Apr-2017.)
Hypotheses
Ref Expression
ax11w.1
ax11w.2
Assertion
Ref Expression
ax11w
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)

Proof of Theorem ax11w
StepHypRef Expression
1 ax11w.2 . . 3
21spw 1679 . 2
3 ax11w.1 . . 3
43ax11wlem 1706 . 2
52, 4syl5 28 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176  wal 1530 This theorem is referenced by:  ax11wdemo  1709 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532
 Copyright terms: Public domain W3C validator