Theorem elequ2 2158

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  elequ2g  2159  elsb2  2160  elequ12  2161  ax12wdemo  2170  dveel2  2494  axextg  2737  axextmo  2739  eleq2w  2847  nfcvf  2951  sbralie  3342  unissb  4906  dftr2c  5221  axrep1  5239  axreplem  5240  axrep4OLD  5245  axsepg  5258  bm1.3iiOLD  5265  exnelv  5276  nalsetOLD  5278  fv3  6899  zfun  7733  tz7.48lem  8424  coflton  8653  aceq1  10097  aceq0  10098  aceq2  10099  dfac2a  10109  kmlem4  10133  axdc3lem2  10430  zfac  10439  nd2  10568  nd3  10569  axrepndlem2  10573  axunndlem1  10575  axunnd  10576  axpowndlem2  10578  axpowndlem3  10579  axpowndlem4  10580  axpownd  10581  axregndlem2  10583  axregnd  10584  axinfndlem1  10585  axacndlem5  10591  zfcndrep  10594  zfcndun  10595  zfcndac  10599  axgroth4  10812  nqereu  10909  mdetunilem9  22777  neiptopnei  23289  2ndc1stc  23608  restlly  23640  kqt0lem  23893  regr1lem2  23897  nrmr0reg  23906  hauspwpwf1  24144  constrcbvlem  34145  dya2iocuni  34673  axprALT2  35503  axsepg2  35553  axsepg3  35554  axsepg3ALT  35555  axsepg4  35556  axsepg5  35557  axnulg  35558  erdsze  35694  untsucf  36202  untangtr  36206  dfon2lem3  36275  dfon2lem6  36278  dfon2lem7  36279  dfon2lem8  36280  dfon2  36282  axextbdist  36290  distel  36293  axextndbi  36294  fness  36860  fneref  36861  axtco1from2  36986  axtcond  36989  axuntco  36990  dfttc4lem2  37040  mh-setindnd  37048  mh-unprimbi  37055  bj-axc14nf  37490  bj-bm1.3ii  37700  matunitlindflem1  38267  prtlem13  39642  prtlem15  39649  prtlem17  39650  dveel2ALT  39713  ax12el  39716  aomclem8  43788  unielss  43945  elintima  44379  mnuprdlem3  44984  ismnushort  45011  axc11next  45116  setcthin  50243