Theorem elequ2 2123

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784

This theorem is referenced by:  elequ2g  2124  elsb2  2125  ax12wdemo  2133  dveel2  2462  axextg  2711  axextmo  2713  eleq2w  2822  nfcvf  2935  axrep1  5206  axreplem  5207  axrep4  5210  axsepg  5219  bm1.3ii  5221  nalset  5232  fv3  6774  zfun  7567  tz7.48lem  8242  aceq1  9804  aceq0  9805  aceq2  9806  dfac2a  9816  kmlem4  9840  axdc3lem2  10138  zfac  10147  nd2  10275  nd3  10276  axrepndlem2  10280  axunndlem1  10282  axunnd  10283  axpowndlem2  10285  axpowndlem3  10286  axpowndlem4  10287  axpownd  10288  axregndlem2  10290  axregnd  10291  axinfndlem1  10292  axacndlem5  10298  zfcndrep  10301  zfcndun  10302  zfcndac  10306  axgroth4  10519  nqereu  10616  mdetunilem9  21677  neiptopnei  22191  2ndc1stc  22510  restlly  22542  kqt0lem  22795  regr1lem2  22799  nrmr0reg  22808  hauspwpwf1  23046  dya2iocuni  32150  erdsze  33064  untsucf  33551  untangtr  33555  dfon2lem3  33667  dfon2lem6  33670  dfon2lem7  33671  dfon2lem8  33672  dfon2  33674  axextbdist  33682  distel  33685  axextndbi  33686  fness  34465  fneref  34466  bj-elequ12  34787  bj-axc14nf  34966  bj-bm1.3ii  35162  matunitlindflem1  35700  prtlem13  36809  prtlem15  36816  prtlem17  36817  dveel2ALT  36880  ax12el  36883  aomclem8  40802  elintima  41150  mnuprdlem3  41781  ismnushort  41808  axc11next  41913  setcthin  46224