Theorem elequ2 2161

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 2160	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2160	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2053	. 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 1943  ax-6 2000  ax-7 2041  ax-9 2156

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

This theorem is used by:  elequ2g  2162  elsb2  2163  elequ12  2164  ax12wdemo  2173  dveel2  2496  axextg  2739  axextmo  2741  eleq2w  2849  nfcvf  2953  sbralie  3344  unissb  4908  dftr2c  5223  axrep1  5241  axreplem  5242  axrep4OLD  5247  axsepg  5260  bm1.3iiOLD  5267  exnelv  5278  nalsetOLD  5280  fv3  6903  zfun  7743  tz7.48lem  8434  coflton  8663  aceq1  10117  aceq0  10118  aceq2  10119  dfac2a  10129  kmlem4  10153  axdc3lem2  10450  zfac  10459  nd2  10590  nd3  10591  axrepndlem2  10595  axunndlem1  10597  axunnd  10598  axpowndlem2  10600  axpowndlem3  10601  axpowndlem4  10602  axpownd  10603  axregndlem2  10605  axregnd  10606  axinfndlem1  10607  axacndlem5  10613  zfcndrep  10616  zfcndun  10617  zfcndac  10621  axgroth4  10834  nqereu  10931  mdetunilem9  22829  neiptopnei  23341  2ndc1stc  23660  restlly  23693  kqt0lem  23946  regr1lem2  23950  nrmr0reg  23959  hauspwpwf1  24197  constrcbvlem  34211  dya2iocuni  34740  axprALT2  35563  axsepg2  35612  axsepg3  35613  axsepg3ALT  35614  axsepg4  35615  axsepg5  35616  axnulg  35617  erdsze  35733  untsucf  36241  untangtr  36245  dfon2lem3  36314  dfon2lem6  36317  dfon2lem7  36318  dfon2lem8  36319  dfon2  36321  axextbdist  36329  distel  36332  axextndbi  36333  fness  36919  fneref  36920  axtco1from2  37045  axtcond  37048  axuntco  37049  dfttc4lem2  37099  mh-setindnd  37107  mh-unprimbi  37114  bj-axc14nf  37549  bj-bm1.3ii  37759  matunitlindflem1  38326  prtlem13  39702  prtlem15  39709  prtlem17  39710  dveel2ALT  39773  ax12el  39776  aomclem8  43848  unielss  44005  elintima  44439  mnuprdlem3  45044  ismnushort  45071  axc11next  45176  setcthin  50302