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

Proof of Theorem nfae
StepHypRef Expression
1 hbae 2041 . 2
21nfi 1561 1
 Colors of variables: wff set class Syntax hints:  wal 1550  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