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

Theorem hba1 1800
Description:  x is not free in  A. x ph. Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Dec-2017.)
Assertion
Ref Expression
hba1  |-  ( A. x ph  ->  A. x A. x ph )

Proof of Theorem hba1
StepHypRef Expression
1 alex 1578 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
2 hbe1 1742 . . 3  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
32hbn 1797 . 2  |-  ( -. 
E. x  -.  ph  ->  A. x  -.  E. x  -.  ph )
41, 3hbxfrbi 1574 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1546   E.wex 1547
This theorem is referenced by:  nfa1  1802  spimehOLD  1836  19.21hOLD  1858  19.12OLD  1866  nfald  1867  cbv3hvOLD  1875  ax12olem5OLD  1981  ax10lem4OLD  1996  ax9OLD  1999  dvelimhOLD  2016  axi5r  2376  axial  2377  hbra1  2715  hbntal  28351  hbimpg  28352  hbimpgVD  28725  hbalgVD  28726  hbexgVD  28727  a9e2eqVD  28728  e2ebindVD  28733  vk15.4jVD  28735  cbv3hvNEW7  29152  19.12vAUX7  29160  ax9NEW7  29174  ax10lem4NEW7  29177  dvelimhvAUX7  29198  dral1NEW7  29199  equs5NEW7  29238  ax7w1AUX7  29345  ax7w4AUX7  29358  19.12OLD7  29370  dvelimhOLD7  29397
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator