Theorem nfae 2433

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

Syntax hints:  ∀wal 1539  Ⅎwnf 1784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2144  ax-11 2160  ax-12 2180  ax-13 2372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfnae  2434  axc16nfALT  2437  dral2  2438  drex2  2442  drnf2  2444  sbequ5  2465  2ax6elem  2470  sbco3  2513  axbnd  2702  axrepnd  10485  axunnd  10487  axpowndlem3  10490  axpownd  10492  axregndlem1  10493  axregnd  10495  axacndlem1  10498  axacndlem2  10499  axacndlem3  10500  axacndlem4  10501  axacndlem5  10502  axacnd  10503