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  3349  unissb  4910  dftr2c  5225  axrep1  5243  axreplem  5244  axrep4OLD  5249  axsepg  5262  bm1.3iiOLD  5267  exnelv  5278  nalsetOLD  5280  fv3  6900  zfun  7734  tz7.48lem  8427  coflton  8656  aceq1  10100  aceq0  10101  aceq2  10102  dfac2a  10112  kmlem4  10136  axdc3lem2  10434  zfac  10443  nd2  10572  nd3  10573  axrepndlem2  10577  axunndlem1  10579  axunnd  10580  axpowndlem2  10582  axpowndlem3  10583  axpowndlem4  10584  axpownd  10585  axregndlem2  10587  axregnd  10588  axinfndlem1  10589  axacndlem5  10595  zfcndrep  10598  zfcndun  10599  zfcndac  10603  axgroth4  10816  nqereu  10913  mdetunilem9  22745  neiptopnei  23257  2ndc1stc  23576  restlly  23608  kqt0lem  23861  regr1lem2  23865  nrmr0reg  23874  hauspwpwf1  24112  constrcbvlem  34089  dya2iocuni  34617  axprALT2  35444  axsepg2  35475  axsepg3  35476  axsepg3ALT  35477  axsepg4  35478  axsepg5  35479  axnulg  35480  erdsze  35592  untsucf  36100  untangtr  36104  dfon2lem3  36173  dfon2lem6  36176  dfon2lem7  36177  dfon2lem8  36178  dfon2  36180  axextbdist  36188  distel  36191  axextndbi  36192  fness  36748  fneref  36749  axtco1from2  36874  axtcond  36877  axuntco  36878  dfttc4lem2  36928  mh-setindnd  36936  mh-unprimbi  36943  bj-axc14nf  37378  bj-bm1.3ii  37587  matunitlindflem1  38154  prtlem13  39531  prtlem15  39538  prtlem17  39539  dveel2ALT  39602  ax12el  39605  aomclem8  43679  unielss  43836  elintima  44270  mnuprdlem3  44875  ismnushort  44902  axc11next  45007  setcthin  50127