Theorem nfae 2437

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

Syntax hints:  ∀wal 1537  Ⅎwnf 1782

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-10 2140  ax-11 2156  ax-12 2176  ax-13 2376

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-nf 1783

This theorem is referenced by:  nfnae  2438  axc16nfALT  2441  dral2  2442  drex2  2446  drnf2  2448  sbequ5  2469  2ax6elem  2474  sbco3  2517  axbnd  2706  axrepnd  10635  axunnd  10637  axpowndlem3  10640  axpownd  10642  axregndlem1  10643  axregnd  10645  axacndlem1  10648  axacndlem2  10649  axacndlem3  10650  axacndlem4  10651  axacndlem5  10652  axacnd  10653