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  2013  ax15  2070  dvelimALT  2183  ax11indn  2245  vk15.4j  28323  a9e2nd  28356  a9e2ndVD  28729  a9e2ndALT  28752  dvelimhwNEW7  29161  ax12olem6NEW7  29165  dvelimvNEW7  29168  dvelimhvAUX7  29198  equs5NEW7  29238  ax15NEW7  29240  a16gNEW7  29250  dvelimALTNEW7  29337
This theorem was proved from axioms:  ax-6 1740
  Copyright terms: Public domain W3C validator