Theorem nfae 2467

Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2406. (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 2465	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2184	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 2179  ax-11 2195  ax-12 2216  ax-13 2406

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  2468  axc16nfALT  2471  dral2  2472  drex2  2476  drnf2  2478  sbequ5  2499  2ax6elem  2504  sbco3  2547  axbnd  2736  axrepnd  10596  axunnd  10598  axpowndlem3  10601  axpownd  10603  axregndlem1  10604  axregnd  10606  axacndlem1  10609  axacndlem2  10610  axacndlem3  10611  axacndlem4  10612  axacndlem5  10613  axacnd  10614  axsepg5  35616  axpowg3  35620  axtcond  37048