Theorem elequ2 2159

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 2158	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2158	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2052	. 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 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154

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

This theorem is used by:  elequ2g  2160  elsb2  2161  elequ12  2162  ax12wdemo  2171  dveel2  2491  axextg  2734  axextmo  2736  eleq2w  2844  nfcvf  2948  sbralie  3338  unissb  4900  dftr2c  5214  axrep1  5232  axreplem  5233  axsepg  5249  exnelv  5266  nalsetOLD  5268  fv3  6908  zfun  7756  tz7.48lemOLD  8459  coflton  8688  aceq1  10203  aceq0  10204  aceq2  10205  dfac2a  10215  kmlem4  10239  axdc3lem2  10536  zfac  10545  nd2  10680  nd3  10681  axrepndlem2  10685  axunndlem1  10687  axunnd  10688  axpowndlem2  10690  axpowndlem3  10691  axpowndlem4  10692  axpownd  10693  axregndlem2  10695  axregnd  10696  axinfndlem1  10697  axacndlem5  10703  zfcndrep  10706  zfcndun  10707  zfcndac  10711  axgroth4  10924  nqereu  11021  mdetunilem9  22944  matunitlindflem1  23003  neiptopnei  23459  2ndc1stc  23778  restlly  23811  kqt0lem  24064  regr1lem2  24068  nrmr0reg  24077  hauspwpwf1  24315  constrcbvlem  34437  dya2iocuni  34965  axprALT2  35792  axsepg2  35876  axsepg3  35877  axsepg3ALT  35878  axsepg4  35879  axsepg5  35880  axnulg  35881  erdsze  36085  untsucf  36599  untangtr  36603  dfon2lem3  36671  dfon2lem6  36674  dfon2lem7  36675  dfon2lem8  36676  dfon2  36678  axextbdist  36686  distel  36689  axextndbi  36690  fness  37261  fneref  37262  axtco1from2  37387  axtcond  37390  axuntco  37391  dfttc4lem2  37441  mh-setindnd  37449  mh-unprimbi  37456  bj-axc14nf  37891  bj-bm1.3ii  38115  prtlem13  40062  prtlem15  40069  prtlem17  40070  dveel2ALT  40133  ax12el  40136  aomclem8  44200  unielss  44357  elintima  44790  mnuprdlem3  45395  ismnushort  45422  axc11next  45527  setcthin  50736