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

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

Proof of Theorem nfae
StepHypRef Expression
1 hbae 2435 . 2 (∀𝑥 𝑥 = 𝑦 → ∀𝑧𝑥 𝑥 = 𝑦)
21nf5i 2145 1 𝑧𝑥 𝑥 = 𝑦
Colors of variables: wff setvar class
Syntax hints:  wal 1537  wnf 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140  ax-11 2156  ax-12 2176  ax-13 2376
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783
This theorem is referenced by:  nfnae  2438  axc16nfALT  2441  dral2  2442  drex2  2446  drnf2  2448  sbequ5  2469  2ax6elem  2474  sbco3  2517  axbnd  2706  axrepnd  10635  axunnd  10637  axpowndlem3  10640  axpownd  10642  axregndlem1  10643  axregnd  10645  axacndlem1  10648  axacndlem2  10649  axacndlem3  10650  axacndlem4  10651  axacndlem5  10652  axacnd  10653
  Copyright terms: Public domain W3C validator