Theorem elequ2 2129

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 2128	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2128	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2022	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124

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

This theorem is referenced by:  elequ2g  2130  elsb2  2131  elequ12  2132  ax12wdemo  2141  dveel2  2467  axextg  2711  axextmo  2713  eleq2w  2821  nfcvf  2926  sbralie  3316  unissb  4884  dftr2c  5196  axrep1  5214  axreplem  5215  axrep4OLD  5220  axsepg  5233  bm1.3iiOLD  5238  exnelv  5249  nalsetOLD  5251  fv3  6853  zfun  7684  tz7.48lem  8374  coflton  8601  aceq1  10033  aceq0  10034  aceq2  10035  dfac2a  10046  kmlem4  10070  axdc3lem2  10367  zfac  10376  nd2  10505  nd3  10506  axrepndlem2  10510  axunndlem1  10512  axunnd  10513  axpowndlem2  10515  axpowndlem3  10516  axpowndlem4  10517  axpownd  10518  axregndlem2  10520  axregnd  10521  axinfndlem1  10522  axacndlem5  10528  zfcndrep  10531  zfcndun  10532  zfcndac  10536  axgroth4  10749  nqereu  10846  mdetunilem9  22598  neiptopnei  23110  2ndc1stc  23429  restlly  23461  kqt0lem  23714  regr1lem2  23718  nrmr0reg  23727  hauspwpwf1  23965  constrcbvlem  33918  dya2iocuni  34446  axsepg2  35244  axsepg2ALT  35245  axnulg  35270  axprALT2  35272  erdsze  35403  untsucf  35911  untangtr  35915  dfon2lem3  35984  dfon2lem6  35987  dfon2lem7  35988  dfon2lem8  35989  dfon2  35991  axextbdist  35999  distel  36002  axextndbi  36003  fness  36550  fneref  36551  axtco1from2  36676  axtcond  36679  axuntco  36680  dfttc4lem2  36730  mh-setindnd  36738  mh-unprimbi  36745  bj-axc14nf  37181  bj-bm1.3ii  37390  matunitlindflem1  37954  prtlem13  39331  prtlem15  39338  prtlem17  39339  dveel2ALT  39402  ax12el  39405  aomclem8  43510  unielss  43667  elintima  44101  mnuprdlem3  44722  ismnushort  44749  axc11next  44854  setcthin  49955