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

Theorem hbn1 1741
Description:  x is not free in  -.  A. x ph. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
Assertion
Ref Expression
hbn1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )

Proof of Theorem hbn1
StepHypRef Expression
1 ax-6 1740 1  |-  ( -. 
A. x ph  ->  A. x  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546
This theorem is referenced by:  hbe1  1742  modal-5  1744  ax5o  1761  hbnOLD  1798  hba1OLD  1801  hbimdOLD  1831  dvelimhwOLD  1873  ax12olem6OLD  1982  dvelimvOLD  1994  a16gOLD  2015  ax15  2074  dvelimALT  2187  ax11indn  2249  vk15.4j  28327  a9e2nd  28360  a9e2ndVD  28733  a9e2ndALT  28756  dvelimhwNEW7  29165  ax12olem6NEW7  29169  dvelimvNEW7  29172  dvelimhvAUX7  29202  equs5NEW7  29242  ax15NEW7  29244  a16gNEW7  29254  dvelimALTNEW7  29341
This theorem was proved from axioms:  ax-6 1740
  Copyright terms: Public domain W3C validator