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  2467  axextg  2710  axextmo  2712  eleq2w  2825  nfcvf  2932  unissb  4939  dftr2c  5262  axrep1  5280  axreplem  5281  axrep4OLD  5286  axsepg  5297  bm1.3iiOLD  5302  nalset  5313  fv3  6924  zfun  7756  tz7.48lem  8481  coflton  8709  aceq1  10157  aceq0  10158  aceq2  10159  dfac2a  10170  kmlem4  10194  axdc3lem2  10491  zfac  10500  nd2  10628  nd3  10629  axrepndlem2  10633  axunndlem1  10635  axunnd  10636  axpowndlem2  10638  axpowndlem3  10639  axpowndlem4  10640  axpownd  10641  axregndlem2  10643  axregnd  10644  axinfndlem1  10645  axacndlem5  10651  zfcndrep  10654  zfcndun  10655  zfcndac  10659  axgroth4  10872  nqereu  10969  mdetunilem9  22626  neiptopnei  23140  2ndc1stc  23459  restlly  23491  kqt0lem  23744  regr1lem2  23748  nrmr0reg  23757  hauspwpwf1  23995  dya2iocuni  34285  axsepg2  35096  axsepg2ALT  35097  axnulg  35106  erdsze  35207  untsucf  35710  untangtr  35714  dfon2lem3  35786  dfon2lem6  35789  dfon2lem7  35790  dfon2lem8  35791  dfon2  35793  axextbdist  35801  distel  35804  axextndbi  35805  fness  36350  fneref  36351  bj-axc14nf  36856  bj-bm1.3ii  37065  matunitlindflem1  37623  prtlem13  38869  prtlem15  38876  prtlem17  38877  dveel2ALT  38940  ax12el  38943  aomclem8  43073  unielss  43230  elintima  43666  mnuprdlem3  44293  ismnushort  44320  axc11next  44425  setcthin  49112