Theorem nfae 2432

Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2371. (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 2430	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2147	1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦

Syntax hints:  ∀wal 1538  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-10 2142  ax-11 2158  ax-12 2178  ax-13 2371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnae  2433  axc16nfALT  2436  dral2  2437  drex2  2441  drnf2  2443  sbequ5  2464  2ax6elem  2469  sbco3  2512  axbnd  2701  axrepnd  10553  axunnd  10555  axpowndlem3  10558  axpownd  10560  axregndlem1  10561  axregnd  10563  axacndlem1  10566  axacndlem2  10567  axacndlem3  10568  axacndlem4  10569  axacndlem5  10570  axacnd  10571