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

Theorem nfae 2432
Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.)
Assertion
Ref Expression
nfae 𝑧𝑥 𝑥 = 𝑦

Proof of Theorem nfae
StepHypRef Expression
1 hbae 2430 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2142 1 𝑧𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  wal 1539  wnf 1785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2371
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786
This theorem is referenced by:  nfnae  2433  axc16nfALT  2436  dral2  2437  drex2  2441  drnf2  2443  sbequ5  2464  2ax6elem  2469  sbco3  2512  axbnd  2702  axrepnd  10585  axunnd  10587  axpowndlem3  10590  axpownd  10592  axregndlem1  10593  axregnd  10595  axacndlem1  10598  axacndlem2  10599  axacndlem3  10600  axacndlem4  10601  axacndlem5  10602  axacnd  10603
  Copyright terms: Public domain W3C validator