Theorem elequ1 2115

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 2114	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2114	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2019	. 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 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110

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

This theorem is referenced by:  elsb1  2116  cleljust  2117  elequ12  2126  ru0  2127  ax12wdemo  2135  cleljustALT  2370  cleljustALT2  2371  dveel1  2469  axc14  2471  sbralie  3366  unissb  4963  dftr2c  5286  axsepgfromrep  5315  nalset  5331  zfpow  5384  dtruALT2  5388  el  5457  dtruOLD  5461  zfun  7771  tz7.48lem  8497  coflton  8727  pssnn  9234  unxpdomlem1  9313  zfinf  9708  aceq1  10186  aceq0  10187  aceq2  10188  dfac3  10190  dfac5lem2  10193  dfac5lem3  10194  dfac2a  10199  kmlem4  10223  zfac  10529  nd1  10656  axextnd  10660  axrepndlem1  10661  axrepndlem2  10662  axunndlem1  10664  axunnd  10665  axpowndlem2  10667  axpowndlem3  10668  axpowndlem4  10669  axregndlem1  10671  axregnd  10673  zfcndun  10684  zfcndpow  10685  zfcndinf  10687  zfcndac  10688  fpwwe2lem11  10710  axgroth3  10900  axgroth4  10901  nqereu  10998  mdetunilem9  22647  madugsum  22670  neiptopnei  23161  2ndc1stc  23480  nrmr0reg  23778  alexsubALTlem4  24079  xrsmopn  24853  itg2cn  25818  itgcn  25900  sqff1o  27243  dya2iocuni  34248  bnj849  34901  axnulg  35068  fineqvrep  35071  erdsze  35170  untsucf  35672  untangtr  35676  dfon2lem3  35749  dfon2lem6  35752  dfon2lem7  35753  dfon2  35756  axextdist  35763  distel  35767  neibastop2lem  36326  bj-nfeel2  36820  prtlem5  38816  prtlem13  38824  prtlem16  38825  ax12el  38898  pw2f1ocnv  42994  aomclem8  43018  onsupmaxb  43200  grumnud  44255  dfnbgr6  47729  lcosslsp  48167