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

Theorem nfae 2349
 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 2348 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2064 1 𝑧𝑥 𝑥 = 𝑦
 Colors of variables: wff setvar class Syntax hints:  ∀wal 1521  Ⅎwnf 1748 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750 This theorem is referenced by:  nfnae  2351  axc16nfALT  2354  dral2  2355  drnf2  2361  sbequ5  2415  sbco3  2445  2ax6elem  2477  sbal  2490  exists1  2590  axi12  2629  axrepnd  9454  axunnd  9456  axpowndlem3  9459  axpownd  9461  axregndlem1  9462  axregnd  9464  axacndlem1  9467  axacndlem2  9468  axacndlem3  9469  axacndlem4  9470  axacndlem5  9471  axacnd  9472
 Copyright terms: Public domain W3C validator