Theorem elequ2 2134

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

Syntax hints:   → wi 4   ↔ wb 207

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  elequ2g  2135  elsb2  2136  elequ12  2137  ax12wdemo  2146  dveel2  2470  axextg  2713  axextmo  2715  eleq2w  2823  nfcvf  2927  sbralie  3317  unissb  4871  dftr2c  5182  axrep1  5200  axreplem  5201  axrep4OLD  5206  axsepg  5219  bm1.3iiOLD  5224  exnelv  5235  nalsetOLD  5237  fv3  6845  zfun  7679  tz7.48lem  8370  coflton  8597  aceq1  10030  aceq0  10031  aceq2  10032  dfac2a  10043  kmlem4  10067  axdc3lem2  10364  zfac  10373  nd2  10502  nd3  10503  axrepndlem2  10507  axunndlem1  10509  axunnd  10510  axpowndlem2  10512  axpowndlem3  10513  axpowndlem4  10514  axpownd  10515  axregndlem2  10517  axregnd  10518  axinfndlem1  10519  axacndlem5  10525  zfcndrep  10528  zfcndun  10529  zfcndac  10533  axgroth4  10746  nqereu  10843  mdetunilem9  22603  neiptopnei  23115  2ndc1stc  23434  restlly  23466  kqt0lem  23719  regr1lem2  23723  nrmr0reg  23732  hauspwpwf1  23970  constrcbvlem  33939  dya2iocuni  34467  axprALT2  35290  axsepg2  35321  axsepg3  35322  axsepg3ALT  35323  axsepg4  35324  axsepg5  35325  axnulg  35326  erdsze  35430  untsucf  35938  untangtr  35942  dfon2lem3  36011  dfon2lem6  36014  dfon2lem7  36015  dfon2lem8  36016  dfon2  36018  axextbdist  36026  distel  36029  axextndbi  36030  fness  36577  fneref  36578  axtco1from2  36703  axtcond  36706  axuntco  36707  dfttc4lem2  36757  mh-setindnd  36765  mh-unprimbi  36772  bj-axc14nf  37208  bj-bm1.3ii  37417  matunitlindflem1  37983  prtlem13  39360  prtlem15  39367  prtlem17  39368  dveel2ALT  39431  ax12el  39434  aomclem8  43506  unielss  43663  elintima  44097  mnuprdlem3  44718  ismnushort  44745  axc11next  44850  setcthin  49955