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  33282  erdsze  34193  untsucf  34679  untangtr  34683  dfon2lem3  34757  dfon2lem6  34760  dfon2lem7  34761  dfon2lem8  34762  dfon2  34764  axextbdist  34772  distel  34775  axextndbi  34776  fness  35234  fneref  35235  bj-elequ12  35556  bj-axc14nf  35734  bj-bm1.3ii  35945  matunitlindflem1  36484  prtlem13  37738  prtlem15  37745  prtlem17  37746  dveel2ALT  37809  ax12el  37812  aomclem8  41803  unielss  41967  elintima  42404  mnuprdlem3  43033  ismnushort  43060  axc11next  43165  setcthin  47675