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

Theorem nfae 2060
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 2059 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1628 1  |-  F/ z A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   A.wal 1396   F/wnf 1621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622
This theorem is referenced by:  nfnae  2062  ax16nfALT  2069  dral2  2070  drnf2  2076  sbequ5  2130  sbco3  2162  2ax6elem  2195  sbal  2208  exists1  2385  axi12  2430  axrepnd  8960  axunnd  8962  axpowndlem3  8965  axpownd  8967  axregndlem1  8968  axregnd  8970  axregndOLD  8971  axacndlem1  8974  axacndlem2  8975  axacndlem3  8976  axacndlem4  8977  axacndlem5  8978  axacnd  8979
  Copyright terms: Public domain W3C validator