Theorem nfae 2451

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

Syntax hints:  ∀wal 1531  Ⅎwnf 1780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-10 2141  ax-11 2156  ax-12 2172  ax-13 2386

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781

This theorem is referenced by:  nfnae  2452  axc16nfALT  2455  dral2  2456  drex2  2460  drnf2  2462  sbequ5  2484  2ax6elem  2489  sbco3  2551  sbalOLD  2571  axi12OLD  2790  axbnd  2791  axrepnd  10010  axunnd  10012  axpowndlem3  10015  axpownd  10017  axregndlem1  10018  axregnd  10020  axacndlem1  10023  axacndlem2  10024  axacndlem3  10025  axacndlem4  10026  axacndlem5  10027  axacnd  10028