Theorem elequ1 2121

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 2120	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2120	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2022	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116

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

This theorem is referenced by:  elsb1  2122  cleljust  2123  elequ12  2132  ru0  2133  ax12wdemo  2141  cleljustALT  2369  cleljustALT2  2370  dveel1  2466  axc14  2468  sbralie  3324  sbralieOLD  3326  unissb  4898  dftr2c  5210  axsepgfromrep  5241  nalset  5260  zfpow  5313  dtruALT2  5317  el  5394  zfun  7691  tz7.48lem  8382  coflton  8609  pssnn  9105  unxpdomlem1  9168  elirrv  9514  zfinf  9560  aceq1  10039  aceq0  10040  aceq2  10041  dfac3  10043  dfac5lem2  10046  dfac5lem3  10047  dfac2a  10052  kmlem4  10076  zfac  10382  nd1  10510  axextnd  10514  axrepndlem1  10515  axrepndlem2  10516  axunndlem1  10518  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axregndlem1  10525  axregnd  10527  zfcndun  10538  zfcndpow  10539  zfcndinf  10541  zfcndac  10542  fpwwe2lem11  10564  axgroth3  10754  axgroth4  10755  nqereu  10852  mdetunilem9  22576  madugsum  22599  neiptopnei  23088  2ndc1stc  23407  nrmr0reg  23705  alexsubALTlem4  24006  xrsmopn  24769  itg2cn  25732  itgcn  25814  sqff1o  27160  dya2iocuni  34460  bnj849  35100  axnulg  35283  fineqvrep  35289  axreg  35302  erdsze  35415  untsucf  35923  untangtr  35927  dfon2lem3  35996  dfon2lem6  35999  dfon2lem7  36000  dfon2  36003  axextdist  36010  distel  36014  neibastop2lem  36573  regsfromregtr  36687  regsfromsetind  36688  bj-nfeel2  37096  bj-axseprep  37316  prtlem5  39230  prtlem13  39238  prtlem16  39239  ax12el  39312  pw2f1ocnv  43388  aomclem8  43412  onsupmaxb  43590  grumnud  44636  dfnbgr6  48211  lcosslsp  48792