Theorem nfae 2463

Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2402. (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 2461	. 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 2402

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  2464  axc16nfALT  2467  dral2  2468  drex2  2472  drnf2  2474  sbequ5  2495  2ax6elem  2500  sbco3  2543  axbnd  2732  axrepnd  10679  axunnd  10681  axpowndlem3  10684  axpownd  10686  axregndlem1  10687  axregnd  10689  axacndlem1  10692  axacndlem2  10693  axacndlem3  10694  axacndlem4  10695  axacndlem5  10696  axacnd  10697  axsepg5  35812  axpowg3  35816  axtcond  37266