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  2368  cleljustALT2  2369  dveel1  2465  axc14  2467  sbralie  3315  sbralieOLD  3317  unissb  4883  dftr2c  5195  axsepgfromrep  5229  exnelv  5248  nalsetOLD  5250  zfpow  5308  dtruALT2  5312  elOLD  5391  zfun  7690  tz7.48lem  8380  coflton  8607  pssnn  9103  unxpdomlem1  9166  elirrv  9512  zfinf  9560  aceq1  10039  aceq0  10040  aceq2  10041  dfac3  10043  dfac5lem2  10046  dfac5lem3  10047  dfac2a  10052  kmlem4  10076  zfac  10382  nd1  10510  axextnd  10514  axrepndlem1  10515  axrepndlem2  10516  axunndlem1  10518  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axregndlem1  10525  axregnd  10527  zfcndun  10538  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  fpwwe2lem11  10564  axgroth3  10754  axgroth4  10755  nqereu  10852  mdetunilem9  22585  madugsum  22608  neiptopnei  23097  2ndc1stc  23416  nrmr0reg  23714  alexsubALTlem4  24015  xrsmopn  24778  itg2cn  25730  itgcn  25812  sqff1o  27145  dya2iocuni  34427  bnj849  35067  axnulg  35251  axprALT2  35253  fineqvrep  35258  axreg  35271  erdsze  35384  untsucf  35892  untangtr  35896  dfon2lem3  35965  dfon2lem6  35968  dfon2lem7  35969  dfon2  35972  axextdist  35979  distel  35983  neibastop2lem  36542  axtco1  36655  axtco2  36656  axtco1from2  36657  axtcond  36660  axuntco  36661  axnulregtco  36662  regsfromregtco  36720  regsfromsetind  36721  mh-prprimbi  36725  mh-unprimbi  36726  mh-regprimbi  36727  mh-infprim2bi  36729  bj-nfeel2  37161  bj-axseprep  37381  prtlem5  39306  prtlem13  39314  prtlem16  39315  ax12el  39388  pw2f1ocnv  43465  aomclem8  43489  onsupmaxb  43667  grumnud  44713  dfnbgr6  48333  lcosslsp  48914