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

Theorem hba1 1805
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 1582 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
2 hbe1 1747 . . 3  |-  ( E. x  -.  ph  ->  A. x E. x  -.  ph )
32hbn 1802 . 2  |-  ( -. 
E. x  -.  ph  ->  A. x  -.  E. x  -.  ph )
41, 3hbxfrbi 1578 1  |-  ( A. x ph  ->  A. x A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1550   E.wex 1551
This theorem is referenced by:  nfa1  1807  spimehOLD  1841  19.21hOLD  1863  19.12OLD  1871  nfald  1872  cbv3hvOLD  1880  ax12olem5OLD  2016  ax10lem4OLD  2031  ax9OLD  2034  dvelimhOLD  2073  axi5r  2411  axial  2412  hbra1  2757  hbntal  28642  hbimpg  28643  hbimpgVD  29018  hbalgVD  29019  hbexgVD  29020  a9e2eqVD  29021  e2ebindVD  29026  vk15.4jVD  29028  cbv3hvNEW7  29448  19.12vAUX7  29456  ax9NEW7  29470  ax10lem4NEW7  29473  dvelimhvAUX7  29494  dral1NEW7  29495  equs5NEW7  29536  sb8iwAUX7  29591  ax7w1AUX7  29647  ax7w4AUX7  29660  19.12OLD7  29688  dvelimhOLD7  29715
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  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator