Theorem elequ2 2157

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

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800

This theorem is referenced by:  elequ2g  2158  elsb2  2159  elequ12  2160  ax12wdemo  2169  dveel2  2493  axextg  2736  axextmo  2738  eleq2w  2846  nfcvf  2950  sbralie  3340  unissb  4899  dftr2c  5210  axrep1  5228  axreplem  5229  axrep4OLD  5234  axsepg  5247  bm1.3iiOLD  5252  exnelv  5263  nalsetOLD  5265  fv3  6885  zfun  7719  tz7.48lem  8412  coflton  8641  aceq1  10073  aceq0  10074  aceq2  10075  dfac2a  10086  kmlem4  10110  axdc3lem2  10408  zfac  10417  nd2  10546  nd3  10547  axrepndlem2  10551  axunndlem1  10553  axunnd  10554  axpowndlem2  10556  axpowndlem3  10557  axpowndlem4  10558  axpownd  10559  axregndlem2  10561  axregnd  10562  axinfndlem1  10563  axacndlem5  10569  zfcndrep  10572  zfcndun  10573  zfcndac  10577  axgroth4  10790  nqereu  10887  mdetunilem9  22680  neiptopnei  23192  2ndc1stc  23511  restlly  23543  kqt0lem  23796  regr1lem2  23800  nrmr0reg  23809  hauspwpwf1  24047  constrcbvlem  34052  dya2iocuni  34580  axprALT2  35405  axsepg2  35436  axsepg3  35437  axsepg3ALT  35438  axsepg4  35439  axsepg5  35440  axnulg  35441  erdsze  35552  untsucf  36060  untangtr  36064  dfon2lem3  36133  dfon2lem6  36136  dfon2lem7  36137  dfon2lem8  36138  dfon2  36140  axextbdist  36148  distel  36151  axextndbi  36152  fness  36709  fneref  36710  axtco1from2  36835  axtcond  36838  axuntco  36839  dfttc4lem2  36889  mh-setindnd  36897  mh-unprimbi  36904  bj-axc14nf  37340  bj-bm1.3ii  37549  matunitlindflem1  38115  prtlem13  39492  prtlem15  39499  prtlem17  39500  dveel2ALT  39563  ax12el  39566  aomclem8  43638  unielss  43795  elintima  44229  mnuprdlem3  44850  ismnushort  44877  axc11next  44982  setcthin  50086