Theorem elequ2 2129

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 2128	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2128	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2022	. 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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124

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

This theorem is referenced by:  elequ2g  2130  elsb2  2131  elequ12  2132  ax12wdemo  2141  dveel2  2466  axextg  2710  axextmo  2712  eleq2w  2820  nfcvf  2925  sbralie  3315  unissb  4883  dftr2c  5195  axrep1  5213  axreplem  5214  axrep4OLD  5219  axsepg  5232  bm1.3iiOLD  5237  exnelv  5248  nalsetOLD  5250  fv3  6858  zfun  7690  tz7.48lem  8380  coflton  8607  aceq1  10039  aceq0  10040  aceq2  10041  dfac2a  10052  kmlem4  10076  axdc3lem2  10373  zfac  10382  nd2  10511  nd3  10512  axrepndlem2  10516  axunndlem1  10518  axunnd  10519  axpowndlem2  10521  axpowndlem3  10522  axpowndlem4  10523  axpownd  10524  axregndlem2  10526  axregnd  10527  axinfndlem1  10528  axacndlem5  10534  zfcndrep  10537  zfcndun  10538  zfcndac  10542  axgroth4  10755  nqereu  10852  mdetunilem9  22585  neiptopnei  23097  2ndc1stc  23416  restlly  23448  kqt0lem  23701  regr1lem2  23705  nrmr0reg  23714  hauspwpwf1  23952  constrcbvlem  33899  dya2iocuni  34427  axsepg2  35225  axsepg2ALT  35226  axnulg  35251  axprALT2  35253  erdsze  35384  untsucf  35892  untangtr  35896  dfon2lem3  35965  dfon2lem6  35968  dfon2lem7  35969  dfon2lem8  35970  dfon2  35972  axextbdist  35980  distel  35983  axextndbi  35984  fness  36531  fneref  36532  axtco1from2  36657  axtcond  36660  axuntco  36661  dfttc4lem2  36711  mh-setindnd  36719  mh-unprimbi  36726  bj-axc14nf  37162  bj-bm1.3ii  37371  matunitlindflem1  37937  prtlem13  39314  prtlem15  39321  prtlem17  39322  dveel2ALT  39385  ax12el  39388  aomclem8  43489  unielss  43646  elintima  44080  mnuprdlem3  44701  ismnushort  44728  axc11next  44833  setcthin  49940