Theorem elequ2 2162

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		ax9 2161	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2161	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2055	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  elequ2g  2163  elsb2  2164  elequ12  2165  ax12wdemo  2174  dveel2  2494  axextg  2737  axextmo  2739  eleq2w  2848  nfcvf  2952  sbralie  3342  unissb  4906  dftr2c  5221  axrep1  5239  axreplem  5240  axsepg  5256  exnelv  5273  nalsetOLD  5275  fv3  6934  zfun  7784  tz7.48lemOLD  8489  coflton  8718  aceq1  10235  aceq0  10236  aceq2  10237  dfac2a  10247  kmlem4  10271  axdc3lem2  10568  zfac  10577  nd2  10712  nd3  10713  axrepndlem2  10717  axunndlem1  10719  axunnd  10720  axpowndlem2  10722  axpowndlem3  10723  axpowndlem4  10724  axpownd  10725  axregndlem2  10727  axregnd  10728  axinfndlem1  10729  axacndlem5  10735  zfcndrep  10738  zfcndun  10739  zfcndac  10743  axgroth4  10956  nqereu  11053  mdetunilem9  22990  matunitlindflem1  23049  neiptopnei  23505  2ndc1stc  23824  restlly  23857  kqt0lem  24110  regr1lem2  24114  nrmr0reg  24123  hauspwpwf1  24361  constrcbvlem  34498  dya2iocuni  35026  axprALT2  35857  axsepg2  35949  axsepg3  35950  axsepg3ALT  35951  axsepg4  35952  axsepg5  35953  axnulg  35954  erdsze  36175  untsucf  36690  untangtr  36694  dfon2lem3  36762  dfon2lem6  36765  dfon2lem7  36766  dfon2lem8  36767  dfon2  36769  axextbdist  36777  distel  36780  axextndbi  36781  fness  37352  fneref  37353  axtco1from2  37478  axtcond  37481  axuntco  37482  dfttc4lem2  37532  mh-setindnd  37540  mh-unprimbi  37547  bj-axc14nf  37982  bj-bm1.3ii  38249  prtlem13  40191  prtlem15  40198  prtlem17  40199  dveel2ALT  40262  ax12el  40265  aomclem8  44329  unielss  44481  elintima  44914  mnuprdlem3  45519  ismnushort  45546  axc11next  45651  setcthin  50931