Theorem elequ1 2113

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 2112	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2112	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2023	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 211	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Syntax hints:   → wi 4   ↔ wb 205

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 1913  ax-6 1971  ax-7 2011  ax-8 2108

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  elsb1  2114  cleljust  2115  ax12wdemo  2131  cleljustALT  2361  cleljustALT2  2362  dveel1  2460  axc14  2462  sbralie  3354  unissb  4943  dftr2c  5268  axsepgfromrep  5297  nalset  5313  zfpow  5364  dtruALT2  5368  el  5437  dtruOLD  5441  zfun  7725  tz7.48lem  8440  coflton  8669  pssnn  9167  unxpdomlem1  9249  pssnnOLD  9264  zfinf  9633  aceq1  10111  aceq0  10112  aceq2  10113  dfac3  10115  dfac5lem2  10118  dfac5lem3  10119  dfac2a  10123  kmlem4  10147  zfac  10454  nd1  10581  axextnd  10585  axrepndlem1  10586  axrepndlem2  10587  axunndlem1  10589  axunnd  10590  axpowndlem2  10592  axpowndlem3  10593  axpowndlem4  10594  axregndlem1  10596  axregnd  10598  zfcndun  10609  zfcndpow  10610  zfcndinf  10612  zfcndac  10613  fpwwe2lem11  10635  axgroth3  10825  axgroth4  10826  nqereu  10923  mdetunilem9  22121  madugsum  22144  neiptopnei  22635  2ndc1stc  22954  nrmr0reg  23252  alexsubALTlem4  23553  xrsmopn  24327  itg2cn  25280  itgcn  25361  sqff1o  26683  dya2iocuni  33277  bnj849  33931  fineqvrep  34090  erdsze  34188  untsucf  34674  untangtr  34678  dfon2lem3  34752  dfon2lem6  34755  dfon2lem7  34756  dfon2  34759  axextdist  34766  distel  34770  neibastop2lem  35240  bj-elequ12  35551  bj-nfeel2  35728  bj-ru0  35818  prtlem5  37725  prtlem13  37733  prtlem16  37734  ax12el  37807  pw2f1ocnv  41766  aomclem8  41793  onsupmaxb  41978  grumnud  43035  lcosslsp  47109