Theorem nfae 2441

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

Syntax hints:  ∀wal 1545  Ⅎwnf 1790

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168  ax-12 2189  ax-13 2380

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfnae  2442  axc16nfALT  2445  dral2  2446  drex2  2450  drnf2  2452  sbequ5  2473  2ax6elem  2478  sbco3  2521  axbnd  2710  axrepnd  10508  axunnd  10510  axpowndlem3  10513  axpownd  10515  axregndlem1  10516  axregnd  10518  axacndlem1  10521  axacndlem2  10522  axacndlem3  10523  axacndlem4  10524  axacndlem5  10525  axacnd  10526  axsepg5  35325  axpowg3  35329  axtcond  36706