Theorem nfae 2464

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

Syntax hints:  ∀wal 1558  Ⅎwnf 1803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-10 2175  ax-11 2191  ax-12 2212  ax-13 2403

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfnae  2465  axc16nfALT  2468  dral2  2469  drex2  2473  drnf2  2475  sbequ5  2496  2ax6elem  2501  sbco3  2544  axbnd  2733  axrepnd  10552  axunnd  10554  axpowndlem3  10557  axpownd  10559  axregndlem1  10560  axregnd  10562  axacndlem1  10565  axacndlem2  10566  axacndlem3  10567  axacndlem4  10568  axacndlem5  10569  axacnd  10570  axsepg5  35440  axpowg3  35444  axtcond  36838