Theorem elequ1 2121

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 2120	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2120	. . 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-8 2116

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

This theorem is referenced by:  elsb1  2122  cleljust  2123  elequ12  2132  ru0  2133  ax12wdemo  2141  cleljustALT  2369  cleljustALT2  2370  dveel1  2466  axc14  2468  sbralie  3316  sbralieOLD  3318  unissb  4884  dftr2c  5196  axsepgfromrep  5229  nalset  5248  zfpow  5301  dtruALT2  5305  elOLD  5384  zfun  7681  tz7.48lem  8371  coflton  8598  pssnn  9094  unxpdomlem1  9157  elirrv  9503  zfinf  9549  aceq1  10028  aceq0  10029  aceq2  10030  dfac3  10032  dfac5lem2  10035  dfac5lem3  10036  dfac2a  10041  kmlem4  10065  zfac  10371  nd1  10499  axextnd  10503  axrepndlem1  10504  axrepndlem2  10505  axunndlem1  10507  axunnd  10508  axpowndlem2  10510  axpowndlem3  10511  axpowndlem4  10512  axregndlem1  10514  axregnd  10516  zfcndun  10527  zfcndpow  10528  zfcndinf  10530  zfcndac  10531  fpwwe2lem11  10553  axgroth3  10743  axgroth4  10744  nqereu  10841  mdetunilem9  22563  madugsum  22586  neiptopnei  23075  2ndc1stc  23394  nrmr0reg  23692  alexsubALTlem4  23993  xrsmopn  24756  itg2cn  25708  itgcn  25790  sqff1o  27132  dya2iocuni  34433  bnj849  35073  axnulg  35257  axprALT2  35259  fineqvrep  35264  axreg  35277  erdsze  35390  untsucf  35898  untangtr  35902  dfon2lem3  35971  dfon2lem6  35974  dfon2lem7  35975  dfon2  35978  axextdist  35985  distel  35989  neibastop2lem  36548  axtco1  36661  axtco2  36662  axtco1from2  36663  axtcond  36666  axuntco  36667  axnultcoreg  36668  regsfromregtco  36726  regsfromsetind  36727  bj-nfeel2  37159  bj-axseprep  37379  prtlem5  39297  prtlem13  39305  prtlem16  39306  ax12el  39379  pw2f1ocnv  43468  aomclem8  43492  onsupmaxb  43670  grumnud  44716  dfnbgr6  48291  lcosslsp  48872