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

Theorem nfae 2111
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 2110 . 2  |-  ( A. x  x  =  y  ->  A. z A. x  x  =  y )
21nfi 1670 1  |-  F/ z A. x  x  =  y
Colors of variables: wff setvar class
Syntax hints:   A.wal 1435   F/wnf 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-nf 1664
This theorem is referenced by:  nfnae  2113  axc16nfALT  2120  dral2  2121  drnf2  2127  sbequ5  2181  sbco3  2211  2ax6elem  2244  sbal  2257  exists1  2359  axi12  2398  axrepnd  9020  axunnd  9022  axpowndlem3  9025  axpownd  9027  axregndlem1  9028  axregnd  9030  axacndlem1  9033  axacndlem2  9034  axacndlem3  9035  axacndlem4  9036  axacndlem5  9037  axacnd  9038
  Copyright terms: Public domain W3C validator