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

Theorem nfae 2315
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 2314 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2021 1 𝑧𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  wal 1478  wnf 1705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707
This theorem is referenced by:  nfnae  2317  axc16nfALT  2322  dral2  2323  drnf2  2329  sbequ5  2386  sbco3  2416  2ax6elem  2448  sbal  2461  exists1  2560  axi12  2599  axrepnd  9368  axunnd  9370  axpowndlem3  9373  axpownd  9375  axregndlem1  9376  axregnd  9378  axacndlem1  9381  axacndlem2  9382  axacndlem3  9383  axacndlem4  9384  axacndlem5  9385  axacnd  9386
  Copyright terms: Public domain W3C validator