Theorem elequ2 2064

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 2063	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2063	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1977	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 204	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743

This theorem is referenced by:  elequ2g  2065  ax12wdemo  2073  dveel2  2399  elsb4  2409  axext3  2752  axext3ALT  2753  axextmo  2755  eleq2w  2849  nfcvf  2958  axrep1  5050  axreplem  5051  axrep4  5054  axsep2  5061  bm1.3ii  5063  nalset  5074  fv3  6517  zfun  7280  tz7.48lem  7880  aceq1  9337  aceq0  9338  aceq2  9339  dfac2a  9349  kmlem4  9373  axdc3lem2  9671  zfac  9680  nd2  9808  nd3  9809  axrepndlem2  9813  axunndlem1  9815  axunnd  9816  axpowndlem2  9818  axpowndlem3  9819  axpowndlem4  9820  axpownd  9821  axregndlem2  9823  axregnd  9824  axinfndlem1  9825  axacndlem5  9831  zfcndrep  9834  zfcndun  9835  zfcndac  9839  axgroth4  10052  nqereu  10149  mdetunilem9  20933  neiptopnei  21444  2ndc1stc  21763  restlly  21795  kqt0lem  22048  regr1lem2  22052  nrmr0reg  22061  hauspwpwf1  22299  dya2iocuni  31192  erdsze  32040  untsucf  32462  untangtr  32466  dfon2lem3  32556  dfon2lem6  32559  dfon2lem7  32560  dfon2lem8  32561  dfon2  32563  axext4dist  32572  distel  32575  axextndbi  32576  fness  33224  fneref  33225  bj-elequ12  33528  bj-axext3  33608  bj-axrep1  33624  bj-axrep2  33625  bj-axrep3  33626  bj-axrep4  33627  bj-axc14nf  33676  bj-axsep2  33743  bj-bm1.3ii  33872  matunitlindflem1  34335  prtlem13  35455  prtlem15  35462  prtlem17  35463  dveel2ALT  35526  ax12el  35529  aomclem8  39063  elintima  39367  mnuprdlem3  39991  axc11next  40161