Theorem nfae 2441

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

Syntax hints:  ∀wal 1535  Ⅎwnf 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2158  ax-12 2178  ax-13 2380

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782

This theorem is referenced by:  nfnae  2442  axc16nfALT  2445  dral2  2446  drex2  2450  drnf2  2452  sbequ5  2473  2ax6elem  2478  sbco3  2521  axbnd  2710  axrepnd  10663  axunnd  10665  axpowndlem3  10668  axpownd  10670  axregndlem1  10671  axregnd  10673  axacndlem1  10676  axacndlem2  10677  axacndlem3  10678  axacndlem4  10679  axacndlem5  10680  axacnd  10681