Theorem eq6 826

Description: All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint).

Assertion

Ref	Expression
eq6	⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)

Proof of Theorem eq6

Step	Hyp	Ref	Expression
1		eq5 824	. 2 ⊢ (∀x x = y → ∀z∀x x = y)
2	1	hbne 699	1 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)

Syntax hints:  ¬ wn 1   → wi 2  ∀wal 672   = weq 797

This theorem is referenced by:  eq6s 827  eqs2 829  eqvin.l1 851  sbequi 876  hbsb4 905  ddelimf2 907  sbidm 912  sbco2 913  sbco3 915  sbcom 916  sbal2 1005  hbeu 1016  ralcom2 1314  axextnd 3737  axrepndlem1 3738  axrepndlem2 3739  axrepnd 3740  axunndlem1 3741  axunnd 3742  axpowndlem2 3744  axpowndlem3 3745  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-12 802

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org