Theorem elequ2 2124

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

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-9 2119

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786

This theorem is referenced by:  elequ2g  2125  elsb2  2126  ax12wdemo  2134  dveel2  2463  axextg  2712  axextmo  2714  eleq2w  2823  nfcvf  2937  axrep1  5214  axreplem  5215  axrep4  5218  axsepg  5227  bm1.3ii  5229  nalset  5240  fv3  6786  zfun  7580  tz7.48lem  8256  aceq1  9857  aceq0  9858  aceq2  9859  dfac2a  9869  kmlem4  9893  axdc3lem2  10191  zfac  10200  nd2  10328  nd3  10329  axrepndlem2  10333  axunndlem1  10335  axunnd  10336  axpowndlem2  10338  axpowndlem3  10339  axpowndlem4  10340  axpownd  10341  axregndlem2  10343  axregnd  10344  axinfndlem1  10345  axacndlem5  10351  zfcndrep  10354  zfcndun  10355  zfcndac  10359  axgroth4  10572  nqereu  10669  mdetunilem9  21750  neiptopnei  22264  2ndc1stc  22583  restlly  22615  kqt0lem  22868  regr1lem2  22872  nrmr0reg  22881  hauspwpwf1  23119  dya2iocuni  32229  erdsze  33143  untsucf  33630  untangtr  33634  dfon2lem3  33740  dfon2lem6  33743  dfon2lem7  33744  dfon2lem8  33745  dfon2  33747  axextbdist  33755  distel  33758  axextndbi  33759  fness  34517  fneref  34518  bj-elequ12  34839  bj-axc14nf  35018  bj-bm1.3ii  35214  matunitlindflem1  35752  prtlem13  36861  prtlem15  36868  prtlem17  36869  dveel2ALT  36932  ax12el  36935  aomclem8  40866  elintima  41214  mnuprdlem3  41845  ismnushort  41872  axc11next  41977  setcthin  46288