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

Theorem nfae 1894
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 1893 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1538 1  |-  F/ z A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   A.wal 1527   F/wnf 1531
This theorem is referenced by:  nfnae  1896  sbequ5  1971  a16nf  1991  sbcom  2029  sbcom2  2053  exists1  2232  axrepnd  8216  axunnd  8218  axpowndlem3  8221  axregndlem1  8224  axregnd  8226  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacndlem5  8233  axacnd  8234
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator