Theorem elequ1 2120

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 2119	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2119	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2021	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

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

This theorem is referenced by:  elsb1  2121  cleljust  2122  elequ12  2131  ru0  2132  ax12wdemo  2140  cleljustALT  2368  cleljustALT2  2369  dveel1  2465  axc14  2467  sbralie  3322  sbralieOLD  3324  unissb  4896  dftr2c  5208  axsepgfromrep  5239  nalset  5258  zfpow  5311  dtruALT2  5315  el  5387  zfun  7681  tz7.48lem  8372  coflton  8599  pssnn  9093  unxpdomlem1  9156  elirrv  9502  zfinf  9548  aceq1  10027  aceq0  10028  aceq2  10029  dfac3  10031  dfac5lem2  10034  dfac5lem3  10035  dfac2a  10040  kmlem4  10064  zfac  10370  nd1  10498  axextnd  10502  axrepndlem1  10503  axrepndlem2  10504  axunndlem1  10506  axunnd  10507  axpowndlem2  10509  axpowndlem3  10510  axpowndlem4  10511  axregndlem1  10513  axregnd  10515  zfcndun  10526  zfcndpow  10527  zfcndinf  10529  zfcndac  10530  fpwwe2lem11  10552  axgroth3  10742  axgroth4  10743  nqereu  10840  mdetunilem9  22564  madugsum  22587  neiptopnei  23076  2ndc1stc  23395  nrmr0reg  23693  alexsubALTlem4  23994  xrsmopn  24757  itg2cn  25720  itgcn  25802  sqff1o  27148  dya2iocuni  34440  bnj849  35081  axnulg  35264  fineqvrep  35270  axreg  35283  erdsze  35396  untsucf  35904  untangtr  35908  dfon2lem3  35977  dfon2lem6  35980  dfon2lem7  35981  dfon2  35984  axextdist  35991  distel  35995  neibastop2lem  36554  regsfromregtr  36668  regsfromsetind  36669  bj-nfeel2  37055  prtlem5  39116  prtlem13  39124  prtlem16  39125  ax12el  39198  pw2f1ocnv  43275  aomclem8  43299  onsupmaxb  43477  grumnud  44523  dfnbgr6  48099  lcosslsp  48680