Theorem nfae 2427

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

Syntax hints:  ∀wal 1531  Ⅎwnf 1777

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-10 2129  ax-11 2146  ax-12 2166  ax-13 2366

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1536  df-ex 1774  df-nf 1778

This theorem is referenced by:  nfnae  2428  axc16nfALT  2431  dral2  2432  drex2  2436  drnf2  2438  sbequ5  2459  2ax6elem  2464  sbco3  2507  axbnd  2697  axrepnd  10623  axunnd  10625  axpowndlem3  10628  axpownd  10630  axregndlem1  10631  axregnd  10633  axacndlem1  10636  axacndlem2  10637  axacndlem3  10638  axacndlem4  10639  axacndlem5  10640  axacnd  10641

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »