Theorem elequ1 2152

Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)

Assertion

Ref	Expression
elequ1	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Proof of Theorem elequ1

Step	Hyp	Ref	Expression
1		ax8 2151	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2151	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2043	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803

This theorem is referenced by:  elsb1  2153  cleljust  2154  elequ12  2163  ru0  2164  ax12wdemo  2172  cleljustALT  2398  cleljustALT2  2399  dveel1  2495  axc14  2497  sbralie  3343  sbralieOLD  3345  unissb  4902  dftr2c  5215  axsepgfromrep  5249  exnelv  5268  nalsetOLD  5270  zfpow  5328  dtruALT2  5332  elOLD  5411  zfun  7723  tz7.48lem  8416  coflton  8645  pssnn  9141  unxpdomlem1  9204  elirrv  9547  elirrvOLD  9548  zfinf  9596  aceq1  10089  aceq0  10090  aceq2  10091  dfac3  10093  dfac5lem2  10096  dfac5lem3  10097  dfac2a  10101  kmlem4  10125  zfac  10432  nd1  10560  axextnd  10564  axrepndlem1  10565  axrepndlem2  10566  axunndlem1  10568  axunnd  10569  axpowndlem2  10571  axpowndlem3  10572  axpowndlem4  10573  axregndlem1  10575  axregnd  10577  zfcndun  10588  zfcndpow  10589  zfcndinf  10591  zfcndac  10592  fpwwe2lem11  10614  axgroth3  10804  axgroth4  10805  nqereu  10902  mdetunilem9  22738  madugsum  22761  neiptopnei  23250  2ndc1stc  23569  nrmr0reg  23867  alexsubALTlem4  24168  xrsmopn  24931  itg2cn  25883  itgcn  25965  sqff1o  27304  dya2iocuni  34590  bnj849  35230  axprALT2  35417  fineqvrep  35422  axreg  35435  axsepg2  35448  axsepg4  35451  axnulg  35453  axpowg  35454  erdsze  35565  untsucf  36073  untangtr  36077  dfon2lem3  36146  dfon2lem6  36149  dfon2lem7  36150  dfon2  36153  axextdist  36160  distel  36164  nmulprop  36553  neibastop2lem  36733  axtco1  36846  axtco2  36847  axtco1from2  36848  axtcond  36851  axuntco  36852  axnulregtco  36853  regsfromregtco  36911  regsfromsetind  36912  mh-prprimbi  36916  mh-unprimbi  36917  mh-regprimbi  36918  mh-infprim2bi  36920  bj-nfeel2  37351  bj-axseprep  37571  prtlem5  39496  prtlem13  39504  prtlem16  39505  ax12el  39578  pw2f1ocnv  43626  aomclem8  43650  onsupmaxb  43828  grumnud  44860  dfnbgr6  48477  lcosslsp  49069