Theorem elequ1 2116

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  elsb1  2117  cleljust  2118  elequ12  2127  ru0  2128  ax12wdemo  2136  cleljustALT  2362  cleljustALT2  2363  dveel1  2459  axc14  2461  sbralie  3326  sbralieOLD  3328  unissb  4903  dftr2c  5217  axsepgfromrep  5249  nalset  5268  zfpow  5321  dtruALT2  5325  el  5397  dtruOLD  5401  zfun  7712  tz7.48lem  8409  coflton  8635  pssnn  9132  unxpdomlem1  9197  zfinf  9592  aceq1  10070  aceq0  10071  aceq2  10072  dfac3  10074  dfac5lem2  10077  dfac5lem3  10078  dfac2a  10083  kmlem4  10107  zfac  10413  nd1  10540  axextnd  10544  axrepndlem1  10545  axrepndlem2  10546  axunndlem1  10548  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axregndlem1  10555  axregnd  10557  zfcndun  10568  zfcndpow  10569  zfcndinf  10571  zfcndac  10572  fpwwe2lem11  10594  axgroth3  10784  axgroth4  10785  nqereu  10882  mdetunilem9  22507  madugsum  22530  neiptopnei  23019  2ndc1stc  23338  nrmr0reg  23636  alexsubALTlem4  23937  xrsmopn  24701  itg2cn  25664  itgcn  25746  sqff1o  27092  dya2iocuni  34274  bnj849  34915  axnulg  35082  fineqvrep  35085  erdsze  35189  untsucf  35697  untangtr  35701  dfon2lem3  35773  dfon2lem6  35776  dfon2lem7  35777  dfon2  35780  axextdist  35787  distel  35791  neibastop2lem  36348  bj-nfeel2  36842  prtlem5  38853  prtlem13  38861  prtlem16  38862  ax12el  38935  pw2f1ocnv  43026  aomclem8  43050  onsupmaxb  43228  grumnud  44275  dfnbgr6  47857  lcosslsp  48427