HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem hbae 1563
Description: All variables are effectively bound in an identical variable specifier.
Assertion
Ref Expression
hbae

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1451 . . . . 5
2 ax-12 1421 . . . . 5
31, 2syl7 63 . . . 4
4 ax10o 1560 . . . . 5
54alequcoms 1427 . . . 4
6 ax10o 1560 . . . . . . 7
76pm2.43i 43 . . . . . 6
8 ax10o 1560 . . . . . 6
97, 8syl5 28 . . . . 5
109alequcoms 1427 . . . 4
113, 5, 10pm2.61ii 155 . . 3
1211a5i 1464 . 2
13 ax-7 1333 . 2
1412, 13syl 15 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1330
This theorem is referenced by:  hbaes 1564  hbnae 1565  dral1 1571  dral2 1572  drex2 1574  sbequ5 1609  aev 1627  hbsb4 1671  sbcom 1681  sbcom2 1767  a12stdy3 1806  exists1 1898  copsexg 3582  axextnd 6799  axrepnd 6802  axunndlem1 6803  axunnd 6804  axpowndlem3 6807  axpownd 6809  axregndlem1 6810  axregnd 6812  axacndlem1 6815  axacndlem2 6816  axacndlem3 6817  axacndlem4 6818  axacndlem5 6819  axacnd 6820  copsexgb 17650  a9e2eq 20908
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-17 1430  ax-9 1445  ax-4 1451
This theorem depends on definitions:  df-bi 175  df-ex 1336
Copyright terms: Public domain