![]() |
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 1910 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax8 1910 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | equcoms 1872 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | impbid 195 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-8 1906 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 |
This theorem is referenced by: cleljust 1912 ax12wdemo 1926 cleljustALT 2102 cleljustALT2 2103 dveel1 2219 axc14 2221 elsb3 2283 axsep 4517 nalset 4533 zfpow 4580 zfun 6603 tz7.48lem 7176 unxpdomlem1 7794 pssnn 7808 zfinf 8162 aceq0 8567 dfac3 8570 dfac5lem2 8573 dfac5lem3 8574 dfac2a 8578 zfac 8908 nd1 9030 axextnd 9034 axrepndlem1 9035 axrepndlem2 9036 axunndlem1 9038 axunnd 9039 axpowndlem2 9041 axpowndlem3 9042 axpowndlem4 9043 axregndlem1 9045 axregnd 9047 zfcndun 9058 zfcndpow 9059 zfcndinf 9061 zfcndac 9062 fpwwe2lem12 9084 axgroth3 9274 axgroth4 9275 nqereu 9372 rpnnen 14356 mdetunilem9 19722 madugsum 19745 neiptopnei 20225 2ndc1stc 20543 nrmr0reg 20841 alexsubALTlem4 21143 xrsmopn 21908 itg2cn 22800 itgcn 22879 sqff1o 24188 dya2iocuni 29178 bnj849 29808 erdsze 29997 untsucf 30409 untangtr 30413 dfon2lem3 30502 dfon2lem6 30505 dfon2lem7 30506 dfon2 30509 axextdist 30517 distel 30521 neibastop2lem 31087 bj-elequ12 31343 bj-axsep 31474 bj-nalset 31475 bj-zfpow 31476 bj-ru0 31607 prtlem5 32494 ax12el 32577 pw2f1ocnv 35963 aomclem8 35990 lcosslsp 40739 |
Copyright terms: Public domain | W3C validator |