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

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

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1450 . . . . 5
2 ax-12 1420 . . . . 5
31, 2syl7 62 . . . 4
4 ax10o 1559 . . . . 5
54alequcoms 1426 . . . 4
6 ax10o 1559 . . . . . . 7
76pm2.43i 42 . . . . . 6
8 ax10o 1559 . . . . . 6
97, 8syl5 27 . . . . 5
109alequcoms 1426 . . . 4
113, 5, 10pm2.61ii 154 . . 3
1211a5i 1463 . 2
13 ax-7 1332 . 2
1412, 13syl 14 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1329
This theorem is referenced by:  hbaes 1563  hbnae 1564  dral1 1570  dral2 1571  drex2 1573  sbequ5 1608  aev 1626  hbsb4 1670  sbcom 1680  sbcom2 1766  a12stdy3 1805  exists1 1897  copsexg 3556  axextnd 6694  axrepnd 6697  axunndlem1 6698  axunnd 6699  axpowndlem3 6702  axpownd 6704  axregndlem1 6705  axregnd 6707  axacndlem1 6710  axacndlem2 6711  axacndlem3 6712  axacndlem4 6713  axacndlem5 6714  axacnd 6715  copsexgb 16538  a9e2eq 19586
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-17 1429  ax-9 1444  ax-4 1450
This theorem depends on definitions:  df-bi 174  df-ex 1335
Copyright terms: Public domain