Theorem elequ2 2128

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 2127	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2127	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2021	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 212	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  elequ2g  2129  elsb2  2130  elequ12  2131  ax12wdemo  2140  dveel2  2466  axextg  2710  axextmo  2712  eleq2w  2820  nfcvf  2925  sbralie  3322  unissb  4896  dftr2c  5208  axrep1  5225  axreplem  5226  axrep4OLD  5231  axsepg  5242  bm1.3iiOLD  5247  nalset  5258  fv3  6852  zfun  7681  tz7.48lem  8372  coflton  8599  aceq1  10027  aceq0  10028  aceq2  10029  dfac2a  10040  kmlem4  10064  axdc3lem2  10361  zfac  10370  nd2  10499  nd3  10500  axrepndlem2  10504  axunndlem1  10506  axunnd  10507  axpowndlem2  10509  axpowndlem3  10510  axpowndlem4  10511  axpownd  10512  axregndlem2  10514  axregnd  10515  axinfndlem1  10516  axacndlem5  10522  zfcndrep  10525  zfcndun  10526  zfcndac  10530  axgroth4  10743  nqereu  10840  mdetunilem9  22564  neiptopnei  23076  2ndc1stc  23395  restlly  23427  kqt0lem  23680  regr1lem2  23684  nrmr0reg  23693  hauspwpwf1  23931  constrcbvlem  33912  dya2iocuni  34440  axsepg2  35238  axsepg2ALT  35239  axnulg  35264  erdsze  35396  untsucf  35904  untangtr  35908  dfon2lem3  35977  dfon2lem6  35980  dfon2lem7  35981  dfon2lem8  35982  dfon2  35984  axextbdist  35992  distel  35995  axextndbi  35996  fness  36543  fneref  36544  mh-setindnd  36667  bj-axc14nf  37056  bj-bm1.3ii  37265  matunitlindflem1  37817  prtlem13  39128  prtlem15  39135  prtlem17  39136  dveel2ALT  39199  ax12el  39202  aomclem8  43303  unielss  43460  elintima  43894  mnuprdlem3  44515  ismnushort  44542  axc11next  44647  setcthin  49710