Theorem elequ2 2122

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 2121	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2121	. . 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783

This theorem is referenced by:  elequ2g  2123  elsb2  2124  ax12wdemo  2132  dveel2  2462  axextg  2706  axextmo  2708  eleq2w  2818  nfcvf  2933  unissb  4944  dftr2c  5269  axrep1  5287  axreplem  5288  axrep4  5291  axsepg  5301  bm1.3ii  5303  nalset  5314  fv3  6910  zfun  7726  tz7.48lem  8441  coflton  8670  aceq1  10112  aceq0  10113  aceq2  10114  dfac2a  10124  kmlem4  10148  axdc3lem2  10446  zfac  10455  nd2  10583  nd3  10584  axrepndlem2  10588  axunndlem1  10590  axunnd  10591  axpowndlem2  10593  axpowndlem3  10594  axpowndlem4  10595  axpownd  10596  axregndlem2  10598  axregnd  10599  axinfndlem1  10600  axacndlem5  10606  zfcndrep  10609  zfcndun  10610  zfcndac  10614  axgroth4  10827  nqereu  10924  mdetunilem9  22122  neiptopnei  22636  2ndc1stc  22955  restlly  22987  kqt0lem  23240  regr1lem2  23244  nrmr0reg  23253  hauspwpwf1  23491  dya2iocuni  33313  erdsze  34224  untsucf  34710  untangtr  34714  dfon2lem3  34788  dfon2lem6  34791  dfon2lem7  34792  dfon2lem8  34793  dfon2  34795  axextbdist  34803  distel  34806  axextndbi  34807  fness  35282  fneref  35283  bj-elequ12  35604  bj-axc14nf  35782  bj-bm1.3ii  35993  matunitlindflem1  36532  prtlem13  37786  prtlem15  37793  prtlem17  37794  dveel2ALT  37857  ax12el  37860  aomclem8  41851  unielss  42015  elintima  42452  mnuprdlem3  43081  ismnushort  43108  axc11next  43213  setcthin  47723