Theorem elequ2 2123

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 2122	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2122	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2019	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118

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

This theorem is referenced by:  elequ2g  2124  elsb2  2125  elequ12  2126  ax12wdemo  2135  dveel2  2466  axextg  2709  axextmo  2711  eleq2w  2818  nfcvf  2925  unissb  4915  dftr2c  5232  axrep1  5250  axreplem  5251  axrep4OLD  5256  axsepg  5267  bm1.3iiOLD  5272  nalset  5283  fv3  6894  zfun  7730  tz7.48lem  8455  coflton  8683  aceq1  10131  aceq0  10132  aceq2  10133  dfac2a  10144  kmlem4  10168  axdc3lem2  10465  zfac  10474  nd2  10602  nd3  10603  axrepndlem2  10607  axunndlem1  10609  axunnd  10610  axpowndlem2  10612  axpowndlem3  10613  axpowndlem4  10614  axpownd  10615  axregndlem2  10617  axregnd  10618  axinfndlem1  10619  axacndlem5  10625  zfcndrep  10628  zfcndun  10629  zfcndac  10633  axgroth4  10846  nqereu  10943  mdetunilem9  22558  neiptopnei  23070  2ndc1stc  23389  restlly  23421  kqt0lem  23674  regr1lem2  23678  nrmr0reg  23687  hauspwpwf1  23925  constrcbvlem  33789  dya2iocuni  34315  axsepg2  35113  axsepg2ALT  35114  axnulg  35123  erdsze  35224  untsucf  35727  untangtr  35731  dfon2lem3  35803  dfon2lem6  35806  dfon2lem7  35807  dfon2lem8  35808  dfon2  35810  axextbdist  35818  distel  35821  axextndbi  35822  fness  36367  fneref  36368  bj-axc14nf  36873  bj-bm1.3ii  37082  matunitlindflem1  37640  prtlem13  38886  prtlem15  38893  prtlem17  38894  dveel2ALT  38957  ax12el  38960  aomclem8  43085  unielss  43242  elintima  43677  mnuprdlem3  44298  ismnushort  44325  axc11next  44430  setcthin  49351