Theorem nfae 2435

Description: All variables are effectively bound in an identical variable specifier. Usage of this theorem is discouraged because it depends on ax-13 2374. (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 2433	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2151	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 2146  ax-11 2162  ax-12 2182  ax-13 2374

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  2436  axc16nfALT  2439  dral2  2440  drex2  2444  drnf2  2446  sbequ5  2467  2ax6elem  2472  sbco3  2515  axbnd  2705  axrepnd  10503  axunnd  10505  axpowndlem3  10508  axpownd  10510  axregndlem1  10511  axregnd  10513  axacndlem1  10516  axacndlem2  10517  axacndlem3  10518  axacndlem4  10519  axacndlem5  10520  axacnd  10521