Theorem elequ2 2121

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 2120	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2120	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2023	. 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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  elequ2g  2122  elsb2  2123  ax12wdemo  2131  dveel2  2460  axextg  2704  axextmo  2706  eleq2w  2816  nfcvf  2931  unissb  4905  dftr2c  5230  axrep1  5248  axreplem  5249  axrep4  5252  axsepg  5262  bm1.3ii  5264  nalset  5275  fv3  6865  zfun  7678  tz7.48lem  8392  coflton  8622  aceq1  10062  aceq0  10063  aceq2  10064  dfac2a  10074  kmlem4  10098  axdc3lem2  10396  zfac  10405  nd2  10533  nd3  10534  axrepndlem2  10538  axunndlem1  10540  axunnd  10541  axpowndlem2  10543  axpowndlem3  10544  axpowndlem4  10545  axpownd  10546  axregndlem2  10548  axregnd  10549  axinfndlem1  10550  axacndlem5  10556  zfcndrep  10559  zfcndun  10560  zfcndac  10564  axgroth4  10777  nqereu  10874  mdetunilem9  22006  neiptopnei  22520  2ndc1stc  22839  restlly  22871  kqt0lem  23124  regr1lem2  23128  nrmr0reg  23137  hauspwpwf1  23375  dya2iocuni  32972  erdsze  33883  untsucf  34368  untangtr  34372  dfon2lem3  34446  dfon2lem6  34449  dfon2lem7  34450  dfon2lem8  34451  dfon2  34453  axextbdist  34461  distel  34464  axextndbi  34465  fness  34897  fneref  34898  bj-elequ12  35219  bj-axc14nf  35397  bj-bm1.3ii  35608  matunitlindflem1  36147  prtlem13  37403  prtlem15  37410  prtlem17  37411  dveel2ALT  37474  ax12el  37477  aomclem8  41446  unielss  41610  elintima  42047  mnuprdlem3  42676  ismnushort  42703  axc11next  42808  setcthin  47195