Theorem nfae 2427

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

Syntax hints:  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2166  ax-13 2366

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfnae  2428  axc16nfALT  2431  dral2  2432  drex2  2436  drnf2  2438  sbequ5  2459  2ax6elem  2464  sbco3  2507  axbnd  2698  axrepnd  10625  axunnd  10627  axpowndlem3  10630  axpownd  10632  axregndlem1  10633  axregnd  10635  axacndlem1  10638  axacndlem2  10639  axacndlem3  10640  axacndlem4  10641  axacndlem5  10642  axacnd  10643