elequ2 - Metamath Proof Explorer

	Metamath Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > elequ2		Structured version Unicode version

Theorem elequ2 1824

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)

**Assertion**
Ref	Expression
elequ2

**Proof of Theorem elequ2**
Step	Hyp	Ref	Expression
1		ax-9 1823	. 2
2		ax-9 1823	. . 3
3	2	equcoms 1796	. 2
4	1, 3	impbid 191	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-9 1823

This theorem depends on definitions: df-bi 185 df-ex 1614

This theorem is referenced by: ax12wdemo 1832 dveel2 2113 elsb4 2180 dveel2ALT 2270 ax12el 2273 axext3 2437 axext3OLD 2438 axext4 2439 bm1.1 2440 bm1.1OLD 2441 axrep1 4569 axrep2 4570 axrep3 4571 axrep4 4572 bm1.3ii 4581 nalset 4593 fv3 5885 zfun 6592 tz7.48lem 7124 aceq0 8516 dfac2a 8527 axdc3lem2 8848 zfac 8857 nd2 8980 nd3 8981 axrepndlem2 8985 axunndlem1 8987 axunnd 8988 axpowndlem2 8990 axpowndlem2OLD 8991 axpowndlem3 8992 axpowndlem3OLD 8993 axpowndlem4 8994 axpownd 8995 axregndlem2 8997 axregnd 8998 axregndOLD 8999 axinfndlem1 9000 axacndlem5 9006 zfcndrep 9009 zfcndun 9010 zfcndac 9014 axgroth4 9227 nqereu 9324 rpnnen 13972 mdetunilem9 19249 neiptopnei 19760 2ndc1stc 20078 kqt0lem 20363 regr1lem2 20367 nrmr0reg 20376 hauspwpwf1 20614 dya2iocuni 28427 erdsze 28843 untsucf 29300 untangtr 29304 dfon2lem3 29434 dfon2lem6 29437 dfon2lem7 29438 dfon2lem8 29439 dfon2 29441 axext4dist 29450 distel 29453 axextndbi 29454 fness 30372 fneref 30373 prtlem13 30814 prtlem15 30821 prtlem17 30822 aomclem8 31211 axc11next 31517 bj-elequ2g 34380 bj-elequ12 34382 bj-axext3 34497 bj-axrep1 34517 bj-axrep2 34518 bj-axrep3 34519 bj-axrep4 34520 bj-nalset 34523 bj-eleq2w 34566 bj-axsep2 34636 elintima 37925