![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > elequ2 | Structured version Visualization version Unicode version |
Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
elequ2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax9 1911 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ax9 1911 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | equcoms 1875 |
. 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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-9 1907 |
This theorem depends on definitions: df-bi 190 df-an 377 df-ex 1675 |
This theorem is referenced by: ax12wdemo 1920 dveel2 2211 elsb4 2275 axext3 2444 axext3ALT 2445 axext4 2446 bm1.1 2447 axrep1 4530 axrep2 4531 axrep3 4532 axrep4 4533 bm1.3ii 4542 nalset 4554 fv3 5901 zfun 6611 tz7.48lem 7184 aceq0 8575 dfac2a 8586 axdc3lem2 8907 zfac 8916 nd2 9039 nd3 9040 axrepndlem2 9044 axunndlem1 9046 axunnd 9047 axpowndlem2 9049 axpowndlem3 9050 axpowndlem4 9051 axpownd 9052 axregndlem2 9054 axregnd 9055 axinfndlem1 9056 axacndlem5 9062 zfcndrep 9065 zfcndun 9066 zfcndac 9070 axgroth4 9283 nqereu 9380 rpnnen 14328 mdetunilem9 19694 neiptopnei 20197 2ndc1stc 20515 kqt0lem 20800 regr1lem2 20804 nrmr0reg 20813 hauspwpwf1 21051 dya2iocuni 29154 erdsze 29974 untsucf 30386 untangtr 30390 dfon2lem3 30480 dfon2lem6 30483 dfon2lem7 30484 dfon2lem8 30485 dfon2 30487 axext4dist 30496 distel 30499 axextndbi 30500 fness 31054 fneref 31055 bj-elequ2g 31320 bj-elequ12 31322 bj-axext3 31429 bj-axrep1 31448 bj-axrep2 31449 bj-axrep3 31450 bj-axrep4 31451 bj-nalset 31454 bj-eleq2w 31501 bj-axsep2 31573 prtlem13 32485 prtlem15 32492 prtlem17 32493 dveel2ALT 32555 ax12el 32558 aomclem8 35964 elintima 36290 axc11next 36801 |
Copyright terms: Public domain | W3C validator |