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

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

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1462 . . . . 5
2 ax-12 1432 . . . . 5
31, 2syl7 62 . . . 4
4 ax10o 1571 . . . . 5
54alequcoms 1438 . . . 4
6 ax10o 1571 . . . . . . 7
76pm2.43i 42 . . . . . 6
8 ax10o 1571 . . . . . 6
97, 8syl5 27 . . . . 5
109alequcoms 1438 . . . 4
113, 5, 10pm2.61ii 154 . . 3
1211a5i 1475 . 2
13 ax-7 1344 . 2
1412, 13syl 14 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1341
This theorem is referenced by:  hbaes 1575  hbnae 1576  dral1 1582  dral2 1583  drex2 1585  sbequ5 1620  aev 1638  hbsb4 1682  sbcom 1692  sbcom2 1778  a12stdy3 1817  exists1 1909  copsexg 3556  axextnd 6592  axrepnd 6595  axunndlem1 6596  axunnd 6597  axpowndlem3 6600  axpownd 6602  axregndlem1 6603  axregnd 6605  axacndlem1 6608  axacndlem2 6609  axacndlem3 6610  axacndlem4 6611  axacndlem5 6612  axacnd 6613  copsexgb 15620  a9e2eq 18412
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-17 1441  ax-9 1456  ax-4 1462
This theorem depends on definitions:  df-bi 175  df-ex 1347
Copyright terms: Public domain