Theorem elequ2 2128

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

Syntax hints:   → wi 4   ↔ wb 206

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781

This theorem is referenced by:  elequ2g  2129  elsb2  2130  elequ12  2131  ax12wdemo  2140  dveel2  2464  axextg  2708  axextmo  2710  eleq2w  2818  nfcvf  2923  sbralie  3320  unissb  4894  dftr2c  5206  axrep1  5223  axreplem  5224  axrep4OLD  5229  axsepg  5240  bm1.3iiOLD  5245  nalset  5256  fv3  6850  zfun  7679  tz7.48lem  8370  coflton  8597  aceq1  10025  aceq0  10026  aceq2  10027  dfac2a  10038  kmlem4  10062  axdc3lem2  10359  zfac  10368  nd2  10497  nd3  10498  axrepndlem2  10502  axunndlem1  10504  axunnd  10505  axpowndlem2  10507  axpowndlem3  10508  axpowndlem4  10509  axpownd  10510  axregndlem2  10512  axregnd  10513  axinfndlem1  10514  axacndlem5  10520  zfcndrep  10523  zfcndun  10524  zfcndac  10528  axgroth4  10741  nqereu  10838  mdetunilem9  22562  neiptopnei  23074  2ndc1stc  23393  restlly  23425  kqt0lem  23678  regr1lem2  23682  nrmr0reg  23691  hauspwpwf1  23929  constrcbvlem  33861  dya2iocuni  34389  axsepg2  35187  axsepg2ALT  35188  axnulg  35213  erdsze  35345  untsucf  35853  untangtr  35857  dfon2lem3  35926  dfon2lem6  35929  dfon2lem7  35930  dfon2lem8  35931  dfon2  35933  axextbdist  35941  distel  35944  axextndbi  35945  fness  36492  fneref  36493  bj-axc14nf  36999  bj-bm1.3ii  37208  matunitlindflem1  37756  prtlem13  39067  prtlem15  39074  prtlem17  39075  dveel2ALT  39138  ax12el  39141  aomclem8  43245  unielss  43402  elintima  43836  mnuprdlem3  44457  ismnushort  44484  axc11next  44589  setcthin  49652