elequ2 - Metamath Proof Explorer

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

Theorem elequ2 1767

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 1766	. 2
2		ax-9 1766	. . 3
3	2	equcoms 1739	. 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 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-9 1766

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

This theorem is referenced by: ax12wdemo 1775 dveel2 2080 elsb4 2157 dveel2ALT 2257 ax12el 2260 axext3 2442 axext3OLD 2443 axext4 2444 bm1.1 2445 bm1.1OLD 2446 axrep1 4554 axrep2 4555 axrep3 4556 axrep4 4557 bm1.3ii 4566 nalset 4579 fv3 5872 zfun 6570 tz7.48lem 7098 aceq0 8490 dfac2a 8501 axdc3lem2 8822 zfac 8831 nd2 8954 nd3 8955 axrepndlem2 8959 axunndlem1 8961 axunnd 8962 axpowndlem2 8964 axpowndlem2OLD 8965 axpowndlem3 8966 axpowndlem3OLD 8967 axpowndlem4 8968 axpownd 8969 axregndlem2 8971 axregnd 8972 axregndOLD 8973 axinfndlem1 8974 axacndlem5 8980 zfcndrep 8983 zfcndun 8984 zfcndac 8988 axgroth4 9201 nqereu 9298 rpnnen 13812 mdetunilem9 18884 neiptopnei 19394 2ndc1stc 19713 kqt0lem 19967 regr1lem2 19971 nrmr0reg 19980 hauspwpwf1 20218 dya2iocuni 27882 erdsze 28274 untsucf 28545 untangtr 28549 dfon2lem3 28782 dfon2lem6 28785 dfon2lem7 28786 dfon2lem8 28787 dfon2 28789 axext4dist 28798 distel 28801 axextndbi 28802 fness 29743 fneref 29745 prtlem13 30202 prtlem15 30209 prtlem17 30210 aomclem8 30602 axc11next 30848 bj-elequ2g 33196 bj-elequ12 33198 bj-axext3 33312 bj-axrep1 33332 bj-axrep2 33333 bj-axrep3 33334 bj-axrep4 33335 bj-nalset 33338 bj-eleq2w 33381 bj-axsep2 33451