Theorem elequ1 2120

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 2119	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2119	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2021	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115

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

This theorem is referenced by:  elsb1  2121  cleljust  2122  elequ12  2131  ru0  2132  ax12wdemo  2140  cleljustALT  2366  cleljustALT2  2367  dveel1  2463  axc14  2465  sbralie  3319  sbralieOLD  3321  unissb  4891  dftr2c  5203  axsepgfromrep  5234  nalset  5253  zfpow  5306  dtruALT2  5310  el  5382  zfun  7675  tz7.48lem  8366  coflton  8592  pssnn  9085  unxpdomlem1  9147  elirrv  9490  zfinf  9536  aceq1  10015  aceq0  10016  aceq2  10017  dfac3  10019  dfac5lem2  10022  dfac5lem3  10023  dfac2a  10028  kmlem4  10052  zfac  10358  nd1  10485  axextnd  10489  axrepndlem1  10490  axrepndlem2  10491  axunndlem1  10493  axunnd  10494  axpowndlem2  10496  axpowndlem3  10497  axpowndlem4  10498  axregndlem1  10500  axregnd  10502  zfcndun  10513  zfcndpow  10514  zfcndinf  10516  zfcndac  10517  fpwwe2lem11  10539  axgroth3  10729  axgroth4  10730  nqereu  10827  mdetunilem9  22536  madugsum  22559  neiptopnei  23048  2ndc1stc  23367  nrmr0reg  23665  alexsubALTlem4  23966  xrsmopn  24729  itg2cn  25692  itgcn  25774  sqff1o  27120  dya2iocuni  34317  bnj849  34958  axnulg  35140  axreg  35146  fineqvrep  35158  erdsze  35267  untsucf  35775  untangtr  35779  dfon2lem3  35848  dfon2lem6  35851  dfon2lem7  35852  dfon2  35855  axextdist  35862  distel  35866  neibastop2lem  36425  bj-nfeel2  36919  prtlem5  38979  prtlem13  38987  prtlem16  38988  ax12el  39061  pw2f1ocnv  43154  aomclem8  43178  onsupmaxb  43356  grumnud  44403  dfnbgr6  47981  lcosslsp  48563