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

Theorem nfae 2482
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 2481 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2191 1 𝑧𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  wal 1635  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfnae  2484  axc16nfALT  2487  dral2  2488  drex2  2492  drnf2  2494  sbequ5  2548  sbco3  2578  2ax6elem  2612  sbal  2625  exists1  2732  axi12  2789  axrepnd  9704  axunnd  9706  axpowndlem3  9709  axpownd  9711  axregndlem1  9712  axregnd  9714  axacndlem1  9717  axacndlem2  9718  axacndlem3  9719  axacndlem4  9720  axacndlem5  9721  axacnd  9722
  Copyright terms: Public domain W3C validator