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

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

Proof of Theorem hbae
StepHypRef Expression
1 ax-4 1563 . . . . 5
2 ax-12 1533 . . . . 5
31, 2syl7 63 . . . 4
4 ax10o 1672 . . . . 5
54alequcoms 1539 . . . 4
6 ax10o 1672 . . . . . . 7
76pm2.43i 43 . . . . . 6
8 ax10o 1672 . . . . . 6
97, 8syl5 28 . . . . 5
109alequcoms 1539 . . . 4
113, 5, 10pm2.61ii 155 . . 3
1211a5i 1576 . 2
13 ax-7 1445 . 2
1412, 13syl 15 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4  wal 1442
This theorem is referenced by:  hbaes 1676  hbnae 1677  dral1 1683  dral2 1684  drex2 1686  sbequ5 1721  aev 1739  hbsb4 1783  sbcom 1793  sbcom2 1879  a12stdy3 1918  exists1 2010  copsexg 3731  axextnd 7434  axrepnd 7437  axunndlem1 7438  axunnd 7439  axpowndlem3 7442  axpownd 7444  axregndlem1 7445  axregnd 7447  axacndlem1 7450  axacndlem2 7451  axacndlem3 7452  axacndlem4 7453  axacndlem5 7454  axacnd 7455  copsexgb 19306  a9e2eq 22187
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-17 1542  ax-9 1557  ax-4 1563
This theorem depends on definitions:  df-bi 175  df-ex 1448
Copyright terms: Public domain