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

Theorem nfae 2043
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 2041 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1561 1  |-  F/ z A. x  x  =  y
Colors of variables: wff set class
Syntax hints:   A.wal 1550   F/wnf 1554
This theorem is referenced by:  nfnae  2045  a16nf  2054  dral2  2056  drnf2  2063  sbequ5  2126  sbcom  2166  sbcomOLD  2167  sbcom2  2192  exists1  2372  axi12  2417  copsexg  4444  axextnd  8468  axrepnd  8471  axunnd  8473  axpowndlem3  8476  axpownd  8478  axregndlem1  8479  axregnd  8481  axacndlem1  8484  axacndlem2  8485  axacndlem3  8486  axacndlem4  8487  axacndlem5  8488  axacnd  8489
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator