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  2492  axextg  2735  axextmo  2737  eleq2w  2845  nfcvf  2949  sbralie  3339  unissb  4901  dftr2c  5215  axrep1  5233  axreplem  5234  axsepg  5250  exnelv  5267  nalsetOLD  5269  fv3  6903  zfun  7752  tz7.48lemOLD  8451  coflton  8680  aceq1  10196  aceq0  10197  aceq2  10198  dfac2a  10208  kmlem4  10232  axdc3lem2  10529  zfac  10538  nd2  10673  nd3  10674  axrepndlem2  10678  axunndlem1  10680  axunnd  10681  axpowndlem2  10683  axpowndlem3  10684  axpowndlem4  10685  axpownd  10686  axregndlem2  10688  axregnd  10689  axinfndlem1  10690  axacndlem5  10696  zfcndrep  10699  zfcndun  10700  zfcndac  10704  axgroth4  10917  nqereu  11014  mdetunilem9  22935  matunitlindflem1  22994  neiptopnei  23450  2ndc1stc  23769  restlly  23802  kqt0lem  24055  regr1lem2  24059  nrmr0reg  24068  hauspwpwf1  24306  constrcbvlem  34387  dya2iocuni  34915  axprALT2  35734  axsepg2  35808  axsepg3  35809  axsepg3ALT  35810  axsepg4  35811  axsepg5  35812  axnulg  35813  erdsze  35967  untsucf  36475  untangtr  36479  dfon2lem3  36547  dfon2lem6  36550  dfon2lem7  36551  dfon2lem8  36552  dfon2  36554  axextbdist  36562  distel  36565  axextndbi  36566  fness  37137  fneref  37138  axtco1from2  37263  axtcond  37266  axuntco  37267  dfttc4lem2  37317  mh-setindnd  37325  mh-unprimbi  37332  bj-axc14nf  37767  bj-bm1.3ii  37979  prtlem13  39925  prtlem15  39932  prtlem17  39933  dveel2ALT  39996  ax12el  39999  aomclem8  44062  unielss  44219  elintima  44652  mnuprdlem3  45257  ismnushort  45284  axc11next  45389  setcthin  50572