Theorem hbnae 1147

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 1145	. 2 |- (A.x x = y -> A.zA.x x = y)
2	1	hbn 1004	1 |- (-. A.x x = y -> A.z -. A.x x = y)

Syntax hints:  -. wn 2   -> wi 3  A.wal 954   = wceq 956

This theorem is referenced by:  hbnaes 1148  dvelimfALT 1153  equvini 1168  sbequ6 1191  equs5 1221  sbequi 1228  hbsb4 1248  sbidm 1254  sbco2 1255  sbco3 1257  sbcom 1258  sbal2 1358  ax11indalem 1368  ax11inda2ALT 1369  hbeu 1389  ralcom2 1776  dfid3 2836  axextnd 4943  axrepndlem1 4944  axrepndlem2 4945  axrepnd 4946  axunndlem1 4947  axunnd 4948  axpowndlem2 4950  axpowndlem3 4951  axpowndlem4 4952  axpownd 4953  axregndlem2 4955  axregnd 4956  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-10 966  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-10o 1140

Copyright terms: Public domain