Theorem nfae 2471

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

Syntax hints:  ∀wal 1565  Ⅎwnf 1810

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-11 2198  ax-12 2219  ax-13 2410

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfnae  2472  axc16nfALT  2475  dral2  2476  drex2  2480  drnf2  2482  sbequ5  2503  2ax6elem  2508  sbco3  2551  axbnd  2740  axrepnd  10579  axunnd  10581  axpowndlem3  10584  axpownd  10586  axregndlem1  10587  axregnd  10589  axacndlem1  10592  axacndlem2  10593  axacndlem3  10594  axacndlem4  10595  axacndlem5  10596  axacnd  10597  axsepg5  35480  axpowg3  35484  axtcond  36878