Theorem nfae 2464

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

This proof depends on syntax axioms:  ∀wal 1567  Ⅎwnf 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-10 2175  ax-11 2191  ax-12 2212  ax-13 2403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1572  df-ex 1809  df-nf 1813

This theorem is used by:  nfnae  2465  axc16nfALT  2468  dral2  2469  drex2  2473  drnf2  2475  sbequ5  2496  2ax6elem  2501  sbco3  2544  axbnd  2733  axrepnd  10585  axunnd  10587  axpowndlem3  10590  axpownd  10592  axregndlem1  10593  axregnd  10595  axacndlem1  10598  axacndlem2  10599  axacndlem3  10600  axacndlem4  10601  axacndlem5  10602  axacnd  10603  axsepg5  35565  axpowg3  35569  axtcond  37017