Theorem elequ1 2154

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 2153	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2153	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2055	. 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 1945  ax-6 2002  ax-7 2043  ax-8 2149

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

This theorem is used by:  elsb1  2155  cleljust  2156  elequ12  2165  ru0  2166  ax12wdemo  2174  cleljustALT  2396  cleljustALT2  2397  dveel1  2493  axc14  2495  sbralie  3342  sbralieOLD  3344  unissb  4904  dftr2c  5219  axsepgfromrep  5251  exnelv  5271  nalsetOLD  5273  zfpow  5333  dtruALT2  5337  el.OLD  5412  zfun  7779  tz7.48lemOLD  8482  coflton  8711  pssnn  9215  unxpdomlem1  9278  elirrv  9621  elirrvOLD  9622  zfinf  9670  aceq1  10226  aceq0  10227  aceq2  10228  dfac3  10230  dfac5lem2  10233  dfac5lem3  10234  dfac2a  10238  kmlem4  10262  zfac  10568  nd1  10702  axextnd  10706  axrepndlem1  10707  axrepndlem2  10708  axunndlem1  10710  axunnd  10711  axpowndlem2  10713  axpowndlem3  10714  axpowndlem4  10715  axregndlem1  10717  axregnd  10719  zfcndun  10730  zfcndpow  10731  zfcndinf  10733  zfcndac  10734  fpwwe2lem11  10756  axgroth3  10946  axgroth4  10947  nqereu  11044  mdetunilem9  22968  madugsum  22991  neiptopnei  23483  2ndc1stc  23802  nrmr0reg  24101  alexsubALTlem4  24402  xrsmopn  25165  itg2cn  26117  itgcn  26198  sqff1o  27542  dya2iocuni  34998  bnj849  35638  axprALT2  35829  fineqvrep  35895  axreg  35908  axsepg2  35921  axsepg4  35924  axnulg  35926  axpowg  35927  erdsze  36147  mirimanofffr  36642  elpssmo  36649  untsucf  36666  untangtr  36670  dfon2lem3  36738  dfon2lem6  36741  dfon2lem7  36742  dfon2  36745  axextdist  36752  distel  36756  nmulprop  37130  neibastop2lem  37339  axtco1  37452  axtco2  37453  axtco1from2  37454  axtcond  37457  axuntco  37458  axnulregtco  37459  regsfromregtco  37517  regsfromsetind  37518  mh-prprimbi  37522  mh-unprimbi  37523  mh-regprimbi  37524  mh-infprim2bi  37526  bj-nfeel2  37957  bj-axseprep  38194  prtlem5  40120  prtlem13  40128  prtlem16  40129  ax12el  40202  pw2f1ocnv  44248  aomclem8  44267  onsupmaxb  44444  grumnud  45473  dfnbgr6  49170  lcosslsp  49765