Theorem nfae 2304

Description: All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)

Assertion

Ref	Expression
nfae	⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦

Proof of Theorem nfae

Step	Hyp	Ref	Expression
1		hbae 2303	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∀𝑧∀𝑥 𝑥 = 𝑦)
2	1	nf5i 2011	1 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦

Syntax hints:  ∀wal 1473  Ⅎwnf 1699

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfnae  2306  axc16nfALT  2311  dral2  2312  drnf2  2318  sbequ5  2375  sbco3  2405  2ax6elem  2437  sbal  2450  exists1  2549  axi12  2588  axrepnd  9295  axunnd  9297  axpowndlem3  9300  axpownd  9302  axregndlem1  9303  axregnd  9305  axacndlem1  9308  axacndlem2  9309  axacndlem3  9310  axacndlem4  9311  axacndlem5  9312  axacnd  9313