Theorem elequ1 2152

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  elsb1  2153  cleljust  2154  elequ12  2163  ru0  2164  ax12wdemo  2172  cleljustALT  2394  cleljustALT2  2395  dveel1  2491  axc14  2493  sbralie  3339  sbralieOLD  3341  unissb  4901  dftr2c  5215  axsepgfromrep  5247  exnelv  5267  nalsetOLD  5269  zfpow  5328  dtruALT2  5332  el.OLD  5407  zfun  7741  tz7.48lemOLD  8435  coflton  8664  pssnn  9168  unxpdomlem1  9231  elirrv  9575  elirrvOLD  9576  zfinf  9624  aceq1  10177  aceq0  10178  aceq2  10179  dfac3  10181  dfac5lem2  10184  dfac5lem3  10185  dfac2a  10189  kmlem4  10213  zfac  10519  nd1  10653  axextnd  10657  axrepndlem1  10658  axrepndlem2  10659  axunndlem1  10661  axunnd  10662  axpowndlem2  10664  axpowndlem3  10665  axpowndlem4  10666  axregndlem1  10668  axregnd  10670  zfcndun  10681  zfcndpow  10682  zfcndinf  10684  zfcndac  10685  fpwwe2lem11  10707  axgroth3  10897  axgroth4  10898  nqereu  10995  mdetunilem9  22915  madugsum  22938  neiptopnei  23430  2ndc1stc  23749  nrmr0reg  24048  alexsubALTlem4  24349  xrsmopn  25112  itg2cn  26064  itgcn  26145  sqff1o  27491  dya2iocuni  34898  bnj849  35538  axprALT2  35713  fineqvrep  35755  axreg  35768  axsepg2  35781  axsepg4  35784  axnulg  35786  axpowg  35787  erdsze  35936  untsucf  36444  untangtr  36448  dfon2lem3  36517  dfon2lem6  36520  dfon2lem7  36521  dfon2  36524  axextdist  36531  distel  36535  nmulprop  36909  neibastop2lem  37118  axtco1  37231  axtco2  37232  axtco1from2  37233  axtcond  37236  axuntco  37237  axnulregtco  37238  regsfromregtco  37296  regsfromsetind  37297  mh-prprimbi  37301  mh-unprimbi  37302  mh-regprimbi  37303  mh-infprim2bi  37305  bj-nfeel2  37736  bj-axseprep  37958  prtlem5  39885  prtlem13  39893  prtlem16  39894  ax12el  39967  pw2f1ocnv  43997  aomclem8  44021  onsupmaxb  44199  grumnud  45229  dfnbgr6  48899  lcosslsp  49494