Theorem elequ2 2004

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 2003	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2003	. . 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-9 1999

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

This theorem is referenced by:  ax12wdemo  2012  dveel2  2371  elsb4  2435  axext3  2604  axext3ALT  2605  axext4  2606  bm1.1  2607  eleq2w  2685  axrep1  4772  axrep2  4773  axrep3  4774  axrep4  4775  axsep2  4782  bm1.3ii  4784  nalset  4795  fv3  6206  zfun  6950  tz7.48lem  7536  aceq1  8940  aceq0  8941  aceq2  8942  dfac2a  8952  kmlem4  8975  axdc3lem2  9273  zfac  9282  nd2  9410  nd3  9411  axrepndlem2  9415  axunndlem1  9417  axunnd  9418  axpowndlem2  9420  axpowndlem3  9421  axpowndlem4  9422  axpownd  9423  axregndlem2  9425  axregnd  9426  axinfndlem1  9427  axacndlem5  9433  zfcndrep  9436  zfcndun  9437  zfcndac  9441  axgroth4  9654  nqereu  9751  mdetunilem9  20426  neiptopnei  20936  2ndc1stc  21254  restlly  21286  kqt0lem  21539  regr1lem2  21543  nrmr0reg  21552  hauspwpwf1  21791  dya2iocuni  30345  erdsze  31184  untsucf  31587  untangtr  31591  dfon2lem3  31690  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  axext4dist  31706  distel  31709  axextndbi  31710  fness  32344  fneref  32345  bj-elequ2g  32666  bj-elequ12  32668  bj-axext3  32769  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axrep4  32791  bj-nalset  32794  bj-axc14nf  32838  bj-axsep2  32921  matunitlindflem1  33405  prtlem13  34153  prtlem15  34160  prtlem17  34161  dveel2ALT  34224  ax12el  34227  aomclem8  37631  elintima  37945  axc11next  38607