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

Theorem nfae 2029
Description: All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfae  |-  F/ z A. x  x  =  y

Proof of Theorem nfae
StepHypRef Expression
1 hbae 2028 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1606 1  |-  F/ z A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   A.wal 1377   F/wnf 1599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by:  nfnae  2031  ax16nfALT  2038  dral2  2039  drnf2  2045  sbequ5  2101  sbcom2OLD  2174  2ax6elem  2179  sbal  2196  exists1  2398  axi12  2443  copsexgOLD  4733  axrepnd  8965  axunnd  8967  axpowndlem3  8971  axpowndlem3OLD  8972  axpownd  8974  axregndlem1  8975  axregnd  8977  axregndOLD  8978  axacndlem1  8981  axacndlem2  8982  axacndlem3  8983  axacndlem4  8984  axacndlem5  8985  axacnd  8986
  Copyright terms: Public domain W3C validator