Theorem elequ2 2160

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 2159	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2159	. . 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 2155

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

This theorem is used by:  elequ2g  2161  elsb2  2162  elequ12  2163  ax12wdemo  2172  dveel2  2491  axextg  2734  axextmo  2736  eleq2w  2844  nfcvf  2948  sbralie  3338  unissb  4901  dftr2c  5215  axrep1  5233  axreplem  5234  axrep4OLD  5239  axsepg  5252  bm1.3iiOLD  5259  exnelv  5270  nalsetOLD  5272  fv3  6897  zfun  7738  tz7.48lem  8431  coflton  8660  aceq1  10121  aceq0  10122  aceq2  10123  dfac2a  10133  kmlem4  10157  axdc3lem2  10454  zfac  10463  nd2  10598  nd3  10599  axrepndlem2  10603  axunndlem1  10605  axunnd  10606  axpowndlem2  10608  axpowndlem3  10609  axpowndlem4  10610  axpownd  10611  axregndlem2  10613  axregnd  10614  axinfndlem1  10615  axacndlem5  10621  zfcndrep  10624  zfcndun  10625  zfcndac  10629  axgroth4  10842  nqereu  10939  mdetunilem9  22843  matunitlindflem1  22902  neiptopnei  23358  2ndc1stc  23677  restlly  23710  kqt0lem  23963  regr1lem2  23967  nrmr0reg  23976  hauspwpwf1  24214  constrcbvlem  34266  dya2iocuni  34795  axprALT2  35618  axsepg2  35667  axsepg3  35668  axsepg3ALT  35669  axsepg4  35670  axsepg5  35671  axnulg  35672  erdsze  35782  untsucf  36290  untangtr  36294  dfon2lem3  36363  dfon2lem6  36366  dfon2lem7  36367  dfon2lem8  36368  dfon2  36370  axextbdist  36378  distel  36381  axextndbi  36382  fness  36969  fneref  36970  axtco1from2  37095  axtcond  37098  axuntco  37099  dfttc4lem2  37149  mh-setindnd  37157  mh-unprimbi  37164  bj-axc14nf  37599  bj-bm1.3ii  37809  prtlem13  39742  prtlem15  39749  prtlem17  39750  dveel2ALT  39813  ax12el  39816  aomclem8  43903  unielss  44060  elintima  44494  mnuprdlem3  45099  ismnushort  45126  axc11next  45231  setcthin  50392