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

Theorem nfae 2161
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 2160 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1685 1  |-  F/ z A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   A.wal 1453   F/wnf 1678
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  nfnae  2163  axc16nfALT  2168  dral2  2169  drnf2  2175  sbequ5  2227  sbco3  2257  2ax6elem  2289  sbal  2302  exists1  2401  axi12  2440  axrepnd  9045  axunnd  9047  axpowndlem3  9050  axpownd  9052  axregndlem1  9053  axregnd  9055  axacndlem1  9058  axacndlem2  9059  axacndlem3  9060  axacndlem4  9061  axacndlem5  9062  axacnd  9063
  Copyright terms: Public domain W3C validator