Theorem elequ1 2106

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 2105	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2105	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2016	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 211	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Syntax hints:   → wi 4   ↔ wb 205

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775

This theorem is referenced by:  elsb1  2107  cleljust  2108  ax12wdemo  2124  cleljustALT  2357  cleljustALT2  2358  dveel1  2456  axc14  2458  sbralie  3350  unissb  4938  dftr2c  5263  axsepgfromrep  5292  nalset  5308  zfpow  5361  dtruALT2  5365  el  5434  dtruOLD  5438  zfun  7736  tz7.48lem  8456  coflton  8686  pssnn  9187  unxpdomlem1  9269  pssnnOLD  9284  zfinf  9657  aceq1  10135  aceq0  10136  aceq2  10137  dfac3  10139  dfac5lem2  10142  dfac5lem3  10143  dfac2a  10147  kmlem4  10171  zfac  10478  nd1  10605  axextnd  10609  axrepndlem1  10610  axrepndlem2  10611  axunndlem1  10613  axunnd  10614  axpowndlem2  10616  axpowndlem3  10617  axpowndlem4  10618  axregndlem1  10620  axregnd  10622  zfcndun  10633  zfcndpow  10634  zfcndinf  10636  zfcndac  10637  fpwwe2lem11  10659  axgroth3  10849  axgroth4  10850  nqereu  10947  mdetunilem9  22516  madugsum  22539  neiptopnei  23030  2ndc1stc  23349  nrmr0reg  23647  alexsubALTlem4  23948  xrsmopn  24722  itg2cn  25687  itgcn  25768  sqff1o  27108  dya2iocuni  33898  bnj849  34551  fineqvrep  34710  erdsze  34807  untsucf  35299  untangtr  35303  dfon2lem3  35376  dfon2lem6  35379  dfon2lem7  35380  dfon2  35383  axextdist  35390  distel  35394  neibastop2lem  35839  bj-elequ12  36150  bj-nfeel2  36326  bj-ru0  36416  prtlem5  38327  prtlem13  38335  prtlem16  38336  ax12el  38409  pw2f1ocnv  42449  aomclem8  42476  onsupmaxb  42658  grumnud  43714  lcosslsp  47497