Theorem elequ2 2114

Description: An identity law for the non-logical predicate. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
elequ2	⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Proof of Theorem elequ2

Step	Hyp	Ref	Expression
1		ax9 2113	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2113	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2016	. 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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775

This theorem is referenced by:  elequ2g  2115  elsb2  2116  ax12wdemo  2124  dveel2  2457  axextg  2701  axextmo  2703  eleq2w  2813  nfcvf  2929  unissb  4942  dftr2c  5268  axrep1  5286  axreplem  5287  axrep4  5290  axsepg  5300  bm1.3ii  5302  nalset  5313  fv3  6915  zfun  7741  tz7.48lem  8462  coflton  8692  aceq1  10141  aceq0  10142  aceq2  10143  dfac2a  10153  kmlem4  10177  axdc3lem2  10475  zfac  10484  nd2  10612  nd3  10613  axrepndlem2  10617  axunndlem1  10619  axunnd  10620  axpowndlem2  10622  axpowndlem3  10623  axpowndlem4  10624  axpownd  10625  axregndlem2  10627  axregnd  10628  axinfndlem1  10629  axacndlem5  10635  zfcndrep  10638  zfcndun  10639  zfcndac  10643  axgroth4  10856  nqereu  10953  mdetunilem9  22535  neiptopnei  23049  2ndc1stc  23368  restlly  23400  kqt0lem  23653  regr1lem2  23657  nrmr0reg  23666  hauspwpwf1  23904  dya2iocuni  33903  erdsze  34812  untsucf  35304  untangtr  35308  dfon2lem3  35381  dfon2lem6  35384  dfon2lem7  35385  dfon2lem8  35386  dfon2  35388  axextbdist  35396  distel  35399  axextndbi  35400  fness  35833  fneref  35834  bj-elequ12  36155  bj-axc14nf  36332  bj-bm1.3ii  36543  matunitlindflem1  37089  prtlem13  38340  prtlem15  38347  prtlem17  38348  dveel2ALT  38411  ax12el  38414  aomclem8  42485  unielss  42646  elintima  43083  mnuprdlem3  43711  ismnushort  43738  axc11next  43843  setcthin  48061