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

Theorem ax11w 1737
 Description: Weak version of ax-11 1762 from which we can prove any ax-11 1762 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 ). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for , see ax11wdemo 1739. (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 1707 . 2
3 ax11w.1 . . 3
43ax11wlem 1736 . 2
52, 4syl5 31 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178  wal 1550 This theorem is referenced by:  ax11wdemo  1739 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688 This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552
 Copyright terms: Public domain W3C validator