Theorem nfae 2438

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

Syntax hints:  ∀wal 1540  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfnae  2439  axc16nfALT  2442  dral2  2443  drex2  2447  drnf2  2449  sbequ5  2470  2ax6elem  2475  sbco3  2518  axbnd  2708  axrepnd  10511  axunnd  10513  axpowndlem3  10516  axpownd  10518  axregndlem1  10519  axregnd  10521  axacndlem1  10524  axacndlem2  10525  axacndlem3  10526  axacndlem4  10527  axacndlem5  10528  axacnd  10529  axtcond  36679