Theorem elequ1 2114

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 2113	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2113	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2024	. 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 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783

This theorem is referenced by:  elsb1  2115  cleljust  2116  ax12wdemo  2132  cleljustALT  2363  cleljustALT2  2364  dveel1  2462  axc14  2464  axsepgfromrep  5222  nalset  5238  zfpow  5290  dtruALT2  5294  el  5358  dtru  5360  zfun  7598  tz7.48lem  8281  pssnn  8960  unxpdomlem1  9036  pssnnOLD  9049  zfinf  9406  aceq1  9882  aceq0  9883  aceq2  9884  dfac3  9886  dfac5lem2  9889  dfac5lem3  9890  dfac2a  9894  kmlem4  9918  zfac  10225  nd1  10352  axextnd  10356  axrepndlem1  10357  axrepndlem2  10358  axunndlem1  10360  axunnd  10361  axpowndlem2  10363  axpowndlem3  10364  axpowndlem4  10365  axregndlem1  10367  axregnd  10369  zfcndun  10380  zfcndpow  10381  zfcndinf  10383  zfcndac  10384  fpwwe2lem11  10406  axgroth3  10596  axgroth4  10597  nqereu  10694  mdetunilem9  21778  madugsum  21801  neiptopnei  22292  2ndc1stc  22611  nrmr0reg  22909  alexsubALTlem4  23210  xrsmopn  23984  itg2cn  24937  itgcn  25018  sqff1o  26340  dya2iocuni  32259  bnj849  32914  fineqvrep  33073  erdsze  33173  untsucf  33660  untangtr  33664  dfon2lem3  33770  dfon2lem6  33773  dfon2lem7  33774  dfon2  33777  axextdist  33784  distel  33788  neibastop2lem  34558  bj-elequ12  34869  bj-nfeel2  35047  bj-ru0  35140  prtlem5  36881  prtlem13  36889  prtlem16  36890  ax12el  36963  pw2f1ocnv  40866  aomclem8  40893  grumnud  41911  lcosslsp  45790