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  2363  cleljustALT2  2364  dveel1  2460  axc14  2462  sbralie  3328  sbralieOLD  3330  unissb  4906  dftr2c  5220  axsepgfromrep  5252  nalset  5271  zfpow  5324  dtruALT2  5328  el  5400  dtruOLD  5404  zfun  7715  tz7.48lem  8412  coflton  8638  pssnn  9138  unxpdomlem1  9204  zfinf  9599  aceq1  10077  aceq0  10078  aceq2  10079  dfac3  10081  dfac5lem2  10084  dfac5lem3  10085  dfac2a  10090  kmlem4  10114  zfac  10420  nd1  10547  axextnd  10551  axrepndlem1  10552  axrepndlem2  10553  axunndlem1  10555  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axregndlem1  10562  axregnd  10564  zfcndun  10575  zfcndpow  10576  zfcndinf  10578  zfcndac  10579  fpwwe2lem11  10601  axgroth3  10791  axgroth4  10792  nqereu  10889  mdetunilem9  22514  madugsum  22537  neiptopnei  23026  2ndc1stc  23345  nrmr0reg  23643  alexsubALTlem4  23944  xrsmopn  24708  itg2cn  25671  itgcn  25753  sqff1o  27099  dya2iocuni  34281  bnj849  34922  axnulg  35089  fineqvrep  35092  erdsze  35196  untsucf  35704  untangtr  35708  dfon2lem3  35780  dfon2lem6  35783  dfon2lem7  35784  dfon2  35787  axextdist  35794  distel  35798  neibastop2lem  36355  bj-nfeel2  36849  prtlem5  38860  prtlem13  38868  prtlem16  38869  ax12el  38942  pw2f1ocnv  43033  aomclem8  43057  onsupmaxb  43235  grumnud  44282  dfnbgr6  47861  lcosslsp  48431