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

Theorem nfae 2029
 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 2028 . 2
21nfi 1606 1
 Colors of variables: wff setvar class Syntax hints:  wal 1377  wnf 1599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600 This theorem is referenced by:  nfnae  2031  ax16nfALT  2038  dral2  2039  drnf2  2045  sbequ5  2101  sbcom2OLD  2174  2ax6elem  2179  sbal  2196  exists1  2398  axi12  2443  copsexgOLD  4733  axrepnd  8965  axunnd  8967  axpowndlem3  8971  axpowndlem3OLD  8972  axpownd  8974  axregndlem1  8975  axregnd  8977  axregndOLD  8978  axacndlem1  8981  axacndlem2  8982  axacndlem3  8983  axacndlem4  8984  axacndlem5  8985  axacnd  8986
 Copyright terms: Public domain W3C validator