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

Theorem nfae 2452
 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 2450 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2143 1 𝑧𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1528  Ⅎwnf 1777 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385 This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778 This theorem is referenced by:  nfnae  2453  axc16nfALT  2456  dral2  2457  drex2  2461  drnf2  2463  sbequ5  2485  2ax6elem  2490  sbco3  2553  sbalOLD  2573  euaeOLD  2747  axi12OLD  2795  axbnd  2796  axrepnd  10010  axunnd  10012  axpowndlem3  10015  axpownd  10017  axregndlem1  10018  axregnd  10020  axacndlem1  10023  axacndlem2  10024  axacndlem3  10025  axacndlem4  10026  axacndlem5  10027  axacnd  10028
 Copyright terms: Public domain W3C validator