Theorem nfae 2431

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

Syntax hints:  ∀wal 1537  Ⅎwnf 1783

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-10 2135  ax-11 2152  ax-12 2169  ax-13 2370

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfnae  2432  axc16nfALT  2435  dral2  2436  drex2  2440  drnf2  2442  sbequ5  2463  2ax6elem  2468  sbco3  2515  axbnd  2706  axrepnd  10396  axunnd  10398  axpowndlem3  10401  axpownd  10403  axregndlem1  10404  axregnd  10406  axacndlem1  10409  axacndlem2  10410  axacndlem3  10411  axacndlem4  10412  axacndlem5  10413  axacnd  10414