Theorem hbnae 1507

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
hbnae	|- (-. A.x x = y -> A.z -. A.x x = y)

Proof of Theorem hbnae

Step	Hyp	Ref	Expression
1		hbae 1505	. 2 |- (A.x x = y -> A.zA.x x = y)
2	1	hbn 1351	1 |- (-. A.x x = y -> A.z -. A.x x = y)

Syntax hints:  -. wn 2   -> wi 3  A.wal 1296   = wceq 1298

This theorem is referenced by:  hbnaes 1508  dvelimfALT 1514  equvini 1531  equviniOLD 1532  sbequ6 1558  equs5 1591  sbequi 1598  hbsb4 1620  sbidmOLD 1628  sbco2 1629  sbco3 1631  sbcom 1632  sbal2 1749  ax11indalem 1759  ax11inda2ALT 1760  eujustALT 1774  hbeu 1782  ralcom2 2244  ralcom2OLD 2245  dfid3 3587  axextnd 6095  axrepndlem1 6096  axrepndlem2 6097  axrepnd 6098  axunndlem1 6099  axunnd 6100  axpowndlem2 6102  axpowndlem3 6103  axpowndlem4 6104  axpownd 6105  axregndlem2 6107  axregnd 6108  axinfndlem1 6109  axinfnd 6110  axacndlem4 6114  axacndlem5 6115  axacnd 6116  axextdist 13866  axext4dist 13867  distel 13870

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-10o 1500

Copyright terms: Public domain