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

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

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1605 . . . . 5
2 ax-12 1537 . . . . 5
31, 2syl7 63 . . . 4
4 ax10o 1712 . . . . 5
54alequcoms 1593 . . . 4
6 ax10o 1712 . . . . . . 7
76pm2.43i 43 . . . . . 6
8 ax10o 1712 . . . . . 6
97, 8syl5 28 . . . . 5
109alequcoms 1593 . . . 4
113, 5, 10pm2.61ii 155 . . 3
1211a5i 1618 . 2
13 ax-7 1448 . 2
1412, 13syl 15 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1445
This theorem is referenced by:  hbaes  1720  hbnae  1721  dral1  1729  dral2  1731  drex2  1734  sbequ5  1769  aev  1787  hbsb4  1835  sbcom  1845  sbcom2  1932  a12stdy3  1972  exists1  2064  copsexg  3792  axextnd  7589  axrepnd  7592  axunndlem1  7593  axunnd  7594  axpowndlem3  7597  axpownd  7599  axregndlem1  7600  axregnd  7602  axacndlem1  7605  axacndlem2  7606  axacndlem3  7607  axacndlem4  7608  axacndlem5  7609  axacnd  7610  copsexgb  19601  a9e2eq  22487
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605
This theorem depends on definitions:  df-bi 175  df-ex 1451
Copyright terms: Public domain