Theorem nfae 2434

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

Syntax hints:  ∀wal 1539  Ⅎwnf 1789

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-10 2140  ax-11 2157  ax-12 2174  ax-13 2373

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-ex 1786  df-nf 1790

This theorem is referenced by:  nfnae  2435  axc16nfALT  2438  dral2  2439  drex2  2443  drnf2  2445  sbequ5  2466  2ax6elem  2471  sbco3  2518  axbnd  2709  axrepnd  10334  axunnd  10336  axpowndlem3  10339  axpownd  10341  axregndlem1  10342  axregnd  10344  axacndlem1  10347  axacndlem2  10348  axacndlem3  10349  axacndlem4  10350  axacndlem5  10351  axacnd  10352