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

Step	Hyp	Ref	Expression
1		hbae 2435	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2151	1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦

Syntax hints:  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162  ax-12 2184  ax-13 2376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnae  2438  axc16nfALT  2441  dral2  2442  drex2  2446  drnf2  2448  sbequ5  2469  2ax6elem  2474  sbco3  2517  axbnd  2707  axrepnd  10505  axunnd  10507  axpowndlem3  10510  axpownd  10512  axregndlem1  10513  axregnd  10515  axacndlem1  10518  axacndlem2  10519  axacndlem3  10520  axacndlem4  10521  axacndlem5  10522  axacnd  10523