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

Theorem nfae 1894
 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 1893 . 2
21nfi 1538 1
 Colors of variables: wff set class Syntax hints:  wal 1527  wnf 1531 This theorem is referenced by:  nfnae  1896  sbequ5  1971  a16nf  1991  sbcom  2029  sbcom2  2053  exists1  2232  axrepnd  8216  axunnd  8218  axpowndlem3  8221  axregndlem1  8224  axregnd  8226  axacndlem1  8229  axacndlem2  8230  axacndlem3  8231  axacndlem4  8232  axacndlem5  8233  axacnd  8234 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866 This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532
 Copyright terms: Public domain W3C validator