Theorem elequ2 2122

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 2121	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2121	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2024	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117

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

This theorem is referenced by:  elequ2g  2123  elsb2  2124  ax12wdemo  2132  dveel2  2463  axextg  2712  axextmo  2714  eleq2w  2823  nfcvf  2937  axrep1  5211  axreplem  5212  axrep4  5215  axsepg  5225  bm1.3ii  5227  nalset  5238  fv3  6801  zfun  7598  tz7.48lem  8281  aceq1  9882  aceq0  9883  aceq2  9884  dfac2a  9894  kmlem4  9918  axdc3lem2  10216  zfac  10225  nd2  10353  nd3  10354  axrepndlem2  10358  axunndlem1  10360  axunnd  10361  axpowndlem2  10363  axpowndlem3  10364  axpowndlem4  10365  axpownd  10366  axregndlem2  10368  axregnd  10369  axinfndlem1  10370  axacndlem5  10376  zfcndrep  10379  zfcndun  10380  zfcndac  10384  axgroth4  10597  nqereu  10694  mdetunilem9  21778  neiptopnei  22292  2ndc1stc  22611  restlly  22643  kqt0lem  22896  regr1lem2  22900  nrmr0reg  22909  hauspwpwf1  23147  dya2iocuni  32259  erdsze  33173  untsucf  33660  untangtr  33664  dfon2lem3  33770  dfon2lem6  33773  dfon2lem7  33774  dfon2lem8  33775  dfon2  33777  axextbdist  33785  distel  33788  axextndbi  33789  fness  34547  fneref  34548  bj-elequ12  34869  bj-axc14nf  35048  bj-bm1.3ii  35244  matunitlindflem1  35782  prtlem13  36889  prtlem15  36896  prtlem17  36897  dveel2ALT  36960  ax12el  36963  aomclem8  40893  elintima  41268  mnuprdlem3  41899  ismnushort  41926  axc11next  42031  setcthin  46347