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 2027	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 214	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 208

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 1970  ax-7 2015  ax-9 2124

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  elsb4  2130  elequ2g  2131  ax12wdemo  2139  dveel2  2485  axextg  2794  axextmo  2796  eleq2w  2894  nfcvf  3002  axrep1  5172  axreplem  5173  axrep4  5176  axsepg  5185  bm1.3ii  5187  nalset  5198  fv3  6669  zfun  7443  tz7.48lem  8058  aceq1  9524  aceq0  9525  aceq2  9526  dfac2a  9536  kmlem4  9560  axdc3lem2  9854  zfac  9863  nd2  9991  nd3  9992  axrepndlem2  9996  axunndlem1  9998  axunnd  9999  axpowndlem2  10001  axpowndlem3  10002  axpowndlem4  10003  axpownd  10004  axregndlem2  10006  axregnd  10007  axinfndlem1  10008  axacndlem5  10014  zfcndrep  10017  zfcndun  10018  zfcndac  10022  axgroth4  10235  nqereu  10332  mdetunilem9  21207  neiptopnei  21718  2ndc1stc  22037  restlly  22069  kqt0lem  22322  regr1lem2  22326  nrmr0reg  22335  hauspwpwf1  22573  dya2iocuni  31543  erdsze  32451  untsucf  32938  untangtr  32942  dfon2lem3  33032  dfon2lem6  33035  dfon2lem7  33036  dfon2lem8  33037  dfon2  33039  axextbdist  33047  distel  33050  axextndbi  33051  fness  33699  fneref  33700  bj-elequ12  34014  bj-axc14nf  34181  bj-bm1.3ii  34368  matunitlindflem1  34917  prtlem13  36031  prtlem15  36038  prtlem17  36039  dveel2ALT  36102  ax12el  36105  aomclem8  39748  elintima  40083  mnuprdlem3  40695  axc11next  40823