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 2182	1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦

This proof depends on syntax axioms:  ∀wal 1567  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by:  nfnae  2463  axc16nfALT  2466  dral2  2467  drex2  2471  drnf2  2473  sbequ5  2494  2ax6elem  2499  sbco3  2542  axbnd  2731  axrepnd  10686  axunnd  10688  axpowndlem3  10691  axpownd  10693  axregndlem1  10694  axregnd  10696  axacndlem1  10699  axacndlem2  10700  axacndlem3  10701  axacndlem4  10702  axacndlem5  10703  axacnd  10704  axsepg5  35880  axpowg3  35884  axtcond  37390