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

Theorem nfae 2006
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 2005 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1597 1  |-  F/ z A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   A.wal 1368   F/wnf 1590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591
This theorem is referenced by:  nfnae  2008  ax16nfALT  2020  dral2  2022  drnf2  2028  sbequ5  2084  sbcom2OLD  2158  2ax6elem  2163  sbal  2180  exists1  2382  axi12  2427  copsexgOLD  4661  axrepnd  8845  axunnd  8847  axpowndlem3  8851  axpowndlem3OLD  8852  axpownd  8854  axregndlem1  8855  axregnd  8857  axregndOLD  8858  axacndlem1  8861  axacndlem2  8862  axacndlem3  8863  axacndlem4  8864  axacndlem5  8865  axacnd  8866
  Copyright terms: Public domain W3C validator