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

Theorem nfae 2056
 Description: All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)
Assertion
Ref Expression
nfae

Proof of Theorem nfae
StepHypRef Expression
1 hbae 2055 . 2
21nfi 1623 1
 Colors of variables: wff setvar class Syntax hints:  A.wal 1393  F/wnf 1616 This theorem is referenced by:  nfnae  2058  ax16nfALT  2065  dral2  2066  drnf2  2072  sbequ5  2128  sbco3  2160  2ax6elem  2193  sbal  2206  exists1  2388  axi12  2433  copsexgOLD  4738  axrepnd  8990  axunnd  8992  axpowndlem3  8996  axpowndlem3OLD  8997  axpownd  8999  axregndlem1  9000  axregnd  9002  axregndOLD  9003  axacndlem1  9006  axacndlem2  9007  axacndlem3  9008  axacndlem4  9009  axacndlem5  9010  axacnd  9011 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator