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  2467  axextg  2711  axextmo  2713  eleq2w  2821  nfcvf  2926  sbralie  3324  unissb  4898  dftr2c  5210  axrep1  5227  axreplem  5228  axrep4OLD  5233  axsepg  5244  bm1.3iiOLD  5249  nalset  5260  fv3  6860  zfun  7691  tz7.48lem  8382  coflton  8609  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  22576  neiptopnei  23088  2ndc1stc  23407  restlly  23439  kqt0lem  23692  regr1lem2  23696  nrmr0reg  23705  hauspwpwf1  23943  constrcbvlem  33933  dya2iocuni  34461  axsepg2  35259  axsepg2ALT  35260  axnulg  35285  axprALT2  35287  erdsze  35418  untsucf  35926  untangtr  35930  dfon2lem3  35999  dfon2lem6  36002  dfon2lem7  36003  dfon2lem8  36004  dfon2  36006  axextbdist  36014  distel  36017  axextndbi  36018  fness  36565  fneref  36566  mh-setindnd  36689  bj-axc14nf  37103  bj-bm1.3ii  37312  matunitlindflem1  37867  prtlem13  39244  prtlem15  39251  prtlem17  39252  dveel2ALT  39315  ax12el  39318  aomclem8  43418  unielss  43575  elintima  44009  mnuprdlem3  44630  ismnushort  44657  axc11next  44762  setcthin  49824