Theorem nfae 2465

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

Syntax hints:  ∀wal 1568  Ⅎwnf 1813

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192  ax-12 2213  ax-13 2404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfnae  2466  axc16nfALT  2469  dral2  2470  drex2  2474  drnf2  2476  sbequ5  2497  2ax6elem  2502  sbco3  2545  axbnd  2734  axrepnd  10574  axunnd  10576  axpowndlem3  10579  axpownd  10581  axregndlem1  10582  axregnd  10584  axacndlem1  10587  axacndlem2  10588  axacndlem3  10589  axacndlem4  10590  axacndlem5  10591  axacnd  10592  axsepg5  35557  axpowg3  35561  axtcond  37009