| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: All variables are effectively bound in an identical variable specifier. |
| Ref | Expression |
|---|---|
| hbae |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-12 1000 |
. . . . 5
| |
| 2 | ax-4 1005 |
. . . . 5
| |
| 3 | 1, 2 | syl7 23 |
. . . 4
|
| 4 | ax-10o 1173 |
. . . . 5
| |
| 5 | 4 | alequcoms 1176 |
. . . 4
|
| 6 | ax-10o 1173 |
. . . . . 6
| |
| 7 | ax-10o 1173 |
. . . . . . 7
| |
| 8 | 7 | pm2.43i 64 |
. . . . . 6
|
| 9 | 6, 8 | syl5 21 |
. . . . 5
|
| 10 | 9 | alequcoms 1176 |
. . . 4
|
| 11 | 3, 5, 10 | pm2.61ii 128 |
. . 3
|
| 12 | 11 | a5i 1021 |
. 2
|
| 13 | ax-7 994 |
. 2
| |
| 14 | 12, 13 | syl 10 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: hbaes 1179 hbnae 1180 dral1 1187 dral2 1188 drex2 1190 equvini 1201 sbequ5 1223 aev 1241 hbsb4 1281 sbcom 1291 a16g 1309 sbcom2 1367 a12stdy3 1407 exists1 1492 axextnd 5032 axrepnd 5035 axunndlem1 5036 axunnd 5037 axpowndlem3 5040 axpownd 5042 axregndlem1 5043 axregnd 5045 axacndlem1 5048 axacndlem2 5049 axacndlem3 5050 axacndlem4 5051 axacndlem5 5052 axacnd 5053 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 994 ax-gen 995 ax-10 998 ax-12 1000 ax-4 1005 ax-5o 1007 ax-10o 1173 |