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

Theorem nfae 1907
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 1906 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1541 1  |-  F/ z A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   A.wal 1530   F/wnf 1534
This theorem is referenced by:  nfnae  1909  sbequ5  1984  a16nf  2004  sbcom  2042  sbcom2  2066  exists1  2245  axrepnd  8232  axunnd  8234  axpowndlem3  8237  axregndlem1  8240  axregnd  8242  axacndlem1  8245  axacndlem2  8246  axacndlem3  8247  axacndlem4  8248  axacndlem5  8249  axacnd  8250
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator