Theorem nfae 2462

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

This proof depends on syntax axioms:  ∀wal 1568  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817

This theorem is used by:  nfnae  2463  axc16nfALT  2466  dral2  2467  drex2  2471  drnf2  2473  sbequ5  2494  2ax6elem  2499  sbco3  2542  axbnd  2731  axrepnd  10604  axunnd  10606  axpowndlem3  10609  axpownd  10611  axregndlem1  10612  axregnd  10614  axacndlem1  10617  axacndlem2  10618  axacndlem3  10619  axacndlem4  10620  axacndlem5  10621  axacnd  10622  axsepg5  35671  axpowg3  35675  axtcond  37098