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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110

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

This theorem is referenced by:  elsb1  2116  cleljust  2117  elequ12  2126  ru0  2127  ax12wdemo  2135  cleljustALT  2367  cleljustALT2  2368  dveel1  2466  axc14  2468  sbralie  3358  unissb  4939  dftr2c  5262  axsepgfromrep  5294  nalset  5313  zfpow  5366  dtruALT2  5370  el  5442  dtruOLD  5446  zfun  7756  tz7.48lem  8481  coflton  8709  pssnn  9208  unxpdomlem1  9286  zfinf  9679  aceq1  10157  aceq0  10158  aceq2  10159  dfac3  10161  dfac5lem2  10164  dfac5lem3  10165  dfac2a  10170  kmlem4  10194  zfac  10500  nd1  10627  axextnd  10631  axrepndlem1  10632  axrepndlem2  10633  axunndlem1  10635  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axregndlem1  10642  axregnd  10644  zfcndun  10655  zfcndpow  10656  zfcndinf  10658  zfcndac  10659  fpwwe2lem11  10681  axgroth3  10871  axgroth4  10872  nqereu  10969  mdetunilem9  22626  madugsum  22649  neiptopnei  23140  2ndc1stc  23459  nrmr0reg  23757  alexsubALTlem4  24058  xrsmopn  24834  itg2cn  25798  itgcn  25880  sqff1o  27225  dya2iocuni  34285  bnj849  34939  axnulg  35106  fineqvrep  35109  erdsze  35207  untsucf  35710  untangtr  35714  dfon2lem3  35786  dfon2lem6  35789  dfon2lem7  35790  dfon2  35793  axextdist  35800  distel  35804  neibastop2lem  36361  bj-nfeel2  36855  prtlem5  38861  prtlem13  38869  prtlem16  38870  ax12el  38943  pw2f1ocnv  43049  aomclem8  43073  onsupmaxb  43251  grumnud  44305  dfnbgr6  47843  lcosslsp  48355