Theorem elequ1 1997

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

Syntax hints:   → wi 4   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  cleljust  1998  ax12wdemo  2012  cleljustALT  2185  cleljustALT2  2186  dveel1  2370  axc14  2372  elsb3  2434  axsep  4780  nalset  4795  zfpow  4844  zfun  6950  tz7.48lem  7536  unxpdomlem1  8164  pssnn  8178  zfinf  8536  aceq0  8941  dfac3  8944  dfac5lem2  8947  dfac5lem3  8948  dfac2a  8952  zfac  9282  nd1  9409  axextnd  9413  axrepndlem1  9414  axrepndlem2  9415  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axregndlem1  9424  axregnd  9426  zfcndun  9437  zfcndpow  9438  zfcndinf  9440  zfcndac  9441  fpwwe2lem12  9463  axgroth3  9653  axgroth4  9654  nqereu  9751  mdetunilem9  20426  madugsum  20449  neiptopnei  20936  2ndc1stc  21254  nrmr0reg  21552  alexsubALTlem4  21854  xrsmopn  22615  itg2cn  23530  itgcn  23609  sqff1o  24908  dya2iocuni  30345  bnj849  30995  erdsze  31184  untsucf  31587  untangtr  31591  dfon2lem3  31690  dfon2lem6  31693  dfon2lem7  31694  dfon2  31697  axextdist  31705  distel  31709  neibastop2lem  32355  bj-elequ12  32668  bj-axsep  32793  bj-nalset  32794  bj-zfpow  32795  bj-nfeel2  32837  bj-ru0  32932  prtlem5  34145  ax12el  34227  pw2f1ocnv  37604  aomclem8  37631  lcosslsp  42227