Theorem nfae 2465

Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2404. (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 2463	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2186	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 1945  ax-6 2002  ax-7 2043  ax-10 2180  ax-11 2197  ax-12 2216  ax-13 2404

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  2466  axc16nfALT  2469  dral2  2470  drex2  2474  drnf2  2476  sbequ5  2497  2ax6elem  2502  sbco3  2545  axbnd  2734  axrepnd  10718  axunnd  10720  axpowndlem3  10723  axpownd  10725  axregndlem1  10726  axregnd  10728  axacndlem1  10731  axacndlem2  10732  axacndlem3  10733  axacndlem4  10734  axacndlem5  10735  axacnd  10736  axsepg5  35953  axpowg3  35957  axtcond  37481