Theorem elequ2 2164

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807

This theorem is referenced by:  elequ2g  2165  elsb2  2166  elequ12  2167  ax12wdemo  2176  dveel2  2500  axextg  2743  axextmo  2745  eleq2w  2853  nfcvf  2957  sbralie  3348  unissb  4908  dftr2c  5223  axrep1  5241  axreplem  5242  axrep4OLD  5247  axsepg  5260  bm1.3iiOLD  5267  exnelv  5278  nalsetOLD  5280  fv3  6900  zfun  7734  tz7.48lem  8428  coflton  8657  aceq1  10101  aceq0  10102  aceq2  10103  dfac2a  10113  kmlem4  10137  axdc3lem2  10435  zfac  10444  nd2  10573  nd3  10574  axrepndlem2  10578  axunndlem1  10580  axunnd  10581  axpowndlem2  10583  axpowndlem3  10584  axpowndlem4  10585  axpownd  10586  axregndlem2  10588  axregnd  10589  axinfndlem1  10590  axacndlem5  10596  zfcndrep  10599  zfcndun  10600  zfcndac  10604  axgroth4  10817  nqereu  10914  mdetunilem9  22746  neiptopnei  23258  2ndc1stc  23577  restlly  23609  kqt0lem  23862  regr1lem2  23866  nrmr0reg  23875  hauspwpwf1  24113  constrcbvlem  34090  dya2iocuni  34618  axprALT2  35446  axsepg2  35486  axsepg3  35487  axsepg3ALT  35488  axsepg4  35489  axsepg5  35490  axnulg  35491  erdsze  35627  untsucf  36135  untangtr  36139  dfon2lem3  36208  dfon2lem6  36211  dfon2lem7  36212  dfon2lem8  36213  dfon2  36215  axextbdist  36223  distel  36226  axextndbi  36227  fness  36783  fneref  36784  axtco1from2  36909  axtcond  36912  axuntco  36913  dfttc4lem2  36963  mh-setindnd  36971  mh-unprimbi  36978  bj-axc14nf  37413  bj-bm1.3ii  37623  matunitlindflem1  38190  prtlem13  39567  prtlem15  39574  prtlem17  39575  dveel2ALT  39638  ax12el  39641  aomclem8  43715  unielss  43872  elintima  44306  mnuprdlem3  44911  ismnushort  44938  axc11next  45043  setcthin  50163