Theorem elequ2 2124

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 2123	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2123	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2020	. 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 2008  ax-9 2119

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

This theorem is referenced by:  elequ2g  2125  elsb2  2126  elequ12  2127  ax12wdemo  2136  dveel2  2461  axextg  2704  axextmo  2706  eleq2w  2813  nfcvf  2919  sbralie  3328  unissb  4906  dftr2c  5220  axrep1  5238  axreplem  5239  axrep4OLD  5244  axsepg  5255  bm1.3iiOLD  5260  nalset  5271  fv3  6879  zfun  7715  tz7.48lem  8412  coflton  8638  aceq1  10077  aceq0  10078  aceq2  10079  dfac2a  10090  kmlem4  10114  axdc3lem2  10411  zfac  10420  nd2  10548  nd3  10549  axrepndlem2  10553  axunndlem1  10555  axunnd  10556  axpowndlem2  10558  axpowndlem3  10559  axpowndlem4  10560  axpownd  10561  axregndlem2  10563  axregnd  10564  axinfndlem1  10565  axacndlem5  10571  zfcndrep  10574  zfcndun  10575  zfcndac  10579  axgroth4  10792  nqereu  10889  mdetunilem9  22514  neiptopnei  23026  2ndc1stc  23345  restlly  23377  kqt0lem  23630  regr1lem2  23634  nrmr0reg  23643  hauspwpwf1  23881  constrcbvlem  33752  dya2iocuni  34281  axsepg2  35079  axsepg2ALT  35080  axnulg  35089  erdsze  35196  untsucf  35704  untangtr  35708  dfon2lem3  35780  dfon2lem6  35783  dfon2lem7  35784  dfon2lem8  35785  dfon2  35787  axextbdist  35795  distel  35798  axextndbi  35799  fness  36344  fneref  36345  bj-axc14nf  36850  bj-bm1.3ii  37059  matunitlindflem1  37617  prtlem13  38868  prtlem15  38875  prtlem17  38876  dveel2ALT  38939  ax12el  38942  aomclem8  43057  unielss  43214  elintima  43649  mnuprdlem3  44270  ismnushort  44297  axc11next  44402  setcthin  49458