![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elequ1 | Structured version Visualization version Unicode version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.) |
Ref | Expression |
---|---|
elequ1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax8 1893 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax8 1893 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | equcoms 1864 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | impbid 194 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 |
This theorem is referenced by: cleljust 1895 ax12wdemo 1909 cleljustALT 2089 cleljustALT2 2090 dveel1 2199 axc14 2201 elsb3 2263 axsep 4524 nalset 4540 zfpow 4582 zfun 6584 tz7.48lem 7158 unxpdomlem1 7776 pssnn 7790 zfinf 8144 aceq0 8549 dfac3 8552 dfac5lem2 8555 dfac5lem3 8556 dfac2a 8560 zfac 8890 nd1 9012 axextnd 9016 axrepndlem1 9017 axrepndlem2 9018 axunndlem1 9020 axunnd 9021 axpowndlem2 9023 axpowndlem3 9024 axpowndlem4 9025 axregndlem1 9027 axregnd 9029 zfcndun 9040 zfcndpow 9041 zfcndinf 9043 zfcndac 9044 fpwwe2lem12 9066 axgroth3 9256 axgroth4 9257 nqereu 9354 rpnnen 14279 mdetunilem9 19645 madugsum 19668 neiptopnei 20148 2ndc1stc 20466 nrmr0reg 20764 alexsubALTlem4 21065 xrsmopn 21830 itg2cn 22721 itgcn 22800 sqff1o 24109 dya2iocuni 29105 bnj849 29736 erdsze 29925 untsucf 30337 untangtr 30341 dfon2lem3 30431 dfon2lem6 30434 dfon2lem7 30435 dfon2 30438 axextdist 30446 distel 30450 neibastop2lem 31016 bj-elequ12 31277 bj-axsep 31408 bj-nalset 31409 bj-zfpow 31410 bj-ru0 31537 prtlem5 32430 ax12el 32513 pw2f1ocnv 35892 aomclem8 35919 lcosslsp 40284 |
Copyright terms: Public domain | W3C validator |