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  2395  cleljustALT2  2396  dveel1  2492  axc14  2494  sbralie  3340  sbralieOLD  3342  unissb  4904  dftr2c  5219  axsepgfromrep  5253  exnelv  5274  nalsetOLD  5276  zfpow  5335  dtruALT2  5339  el.OLD  5418  zfun  7741  tz7.48lem  8434  coflton  8663  pssnn  9167  unxpdomlem1  9230  elirrv  9573  elirrvOLD  9574  zfinf  9622  aceq1  10124  aceq0  10125  aceq2  10126  dfac3  10128  dfac5lem2  10131  dfac5lem3  10132  dfac2a  10136  kmlem4  10160  zfac  10466  nd1  10600  axextnd  10604  axrepndlem1  10605  axrepndlem2  10606  axunndlem1  10608  axunnd  10609  axpowndlem2  10611  axpowndlem3  10612  axpowndlem4  10613  axregndlem1  10615  axregnd  10617  zfcndun  10628  zfcndpow  10629  zfcndinf  10631  zfcndac  10632  fpwwe2lem11  10654  axgroth3  10844  axgroth4  10845  nqereu  10942  mdetunilem9  22848  madugsum  22871  neiptopnei  23363  2ndc1stc  23682  nrmr0reg  23981  alexsubALTlem4  24282  xrsmopn  25045  itg2cn  25997  itgcn  26079  sqff1o  27426  dya2iocuni  34802  bnj849  35442  axprALT2  35625  fineqvrep  35648  axreg  35661  axsepg2  35674  axsepg4  35677  axnulg  35679  axpowg  35680  erdsze  35789  untsucf  36297  untangtr  36301  dfon2lem3  36370  dfon2lem6  36373  dfon2lem7  36374  dfon2  36377  axextdist  36384  distel  36388  nmulprop  36778  neibastop2lem  36987  axtco1  37100  axtco2  37101  axtco1from2  37102  axtcond  37105  axuntco  37106  axnulregtco  37107  regsfromregtco  37165  regsfromsetind  37166  mh-prprimbi  37170  mh-unprimbi  37171  mh-regprimbi  37172  mh-infprim2bi  37174  bj-nfeel2  37605  bj-axseprep  37827  prtlem5  39741  prtlem13  39749  prtlem16  39750  ax12el  39823  pw2f1ocnv  43886  aomclem8  43910  onsupmaxb  44088  grumnud  45118  dfnbgr6  48781  lcosslsp  49376