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  exnelv  5248  nalsetOLD  5250  zfpow  5303  dtruALT2  5307  elOLD  5386  zfun  7683  tz7.48lem  8373  coflton  8600  pssnn  9096  unxpdomlem1  9159  elirrv  9505  zfinf  9551  aceq1  10030  aceq0  10031  aceq2  10032  dfac3  10034  dfac5lem2  10037  dfac5lem3  10038  dfac2a  10043  kmlem4  10067  zfac  10373  nd1  10501  axextnd  10505  axrepndlem1  10506  axrepndlem2  10507  axunndlem1  10509  axunnd  10510  axpowndlem2  10512  axpowndlem3  10513  axpowndlem4  10514  axregndlem1  10516  axregnd  10518  zfcndun  10529  zfcndpow  10530  zfcndinf  10532  zfcndac  10533  fpwwe2lem11  10555  axgroth3  10745  axgroth4  10746  nqereu  10843  mdetunilem9  22595  madugsum  22618  neiptopnei  23107  2ndc1stc  23426  nrmr0reg  23724  alexsubALTlem4  24025  xrsmopn  24788  itg2cn  25740  itgcn  25822  sqff1o  27159  dya2iocuni  34443  bnj849  35083  axnulg  35267  axprALT2  35269  fineqvrep  35274  axreg  35287  erdsze  35400  untsucf  35908  untangtr  35912  dfon2lem3  35981  dfon2lem6  35984  dfon2lem7  35985  dfon2  35988  axextdist  35995  distel  35999  neibastop2lem  36558  axtco1  36671  axtco2  36672  axtco1from2  36673  axtcond  36676  axuntco  36677  axnulregtco  36678  regsfromregtco  36736  regsfromsetind  36737  mh-prprimbi  36741  mh-unprimbi  36742  mh-regprimbi  36743  mh-infprim2bi  36745  bj-nfeel2  37177  bj-axseprep  37397  prtlem5  39320  prtlem13  39328  prtlem16  39329  ax12el  39402  pw2f1ocnv  43483  aomclem8  43507  onsupmaxb  43685  grumnud  44731  dfnbgr6  48345  lcosslsp  48926