MPE Home 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  x and  y be distinct (unless  x does not occur in  ph). For an example of how the hypotheses can be eliminated when we substitute an expression without wff variables for  ph, see ax11wdemo 1739. (Contributed by NM, 10-Apr-2017.)
Hypotheses
Ref Expression
ax11w.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
ax11w.2  |-  ( y  =  z  ->  ( ph 
<->  ch ) )
Assertion
Ref Expression
ax11w  |-  ( x  =  y  ->  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) ) )
Distinct variable groups:    y, z    ps, x    ph, z    ch, y
Allowed substitution hints:    ph( x, y)    ps( y, z)    ch( x, z)

Proof of Theorem ax11w
StepHypRef Expression
1 ax11w.2 . . 3  |-  ( y  =  z  ->  ( ph 
<->  ch ) )
21spw 1707 . 2  |-  ( A. y ph  ->  ph )
3 ax11w.1 . . 3  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
43ax11wlem 1736 . 2  |-  ( x  =  y  ->  ( ph  ->  A. x ( x  =  y  ->  ph )
) )
52, 4syl5 31 1  |-  ( x  =  y  ->  ( A. y ph  ->  A. x
( x  =  y  ->  ph ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178   A.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