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 2027	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 214	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781

This theorem is referenced by:  elsb4  2130  elequ2g  2131  ax12wdemo  2139  dveel2  2485  axextg  2797  axextmo  2799  eleq2w  2898  nfcvf  3009  axrep1  5193  axreplem  5194  axrep4  5197  axsepg  5206  bm1.3ii  5208  nalset  5219  fv3  6690  zfun  7464  tz7.48lem  8079  aceq1  9545  aceq0  9546  aceq2  9547  dfac2a  9557  kmlem4  9581  axdc3lem2  9875  zfac  9884  nd2  10012  nd3  10013  axrepndlem2  10017  axunndlem1  10019  axunnd  10020  axpowndlem2  10022  axpowndlem3  10023  axpowndlem4  10024  axpownd  10025  axregndlem2  10027  axregnd  10028  axinfndlem1  10029  axacndlem5  10035  zfcndrep  10038  zfcndun  10039  zfcndac  10043  axgroth4  10256  nqereu  10353  mdetunilem9  21231  neiptopnei  21742  2ndc1stc  22061  restlly  22093  kqt0lem  22346  regr1lem2  22350  nrmr0reg  22359  hauspwpwf1  22597  dya2iocuni  31543  erdsze  32451  untsucf  32938  untangtr  32942  dfon2lem3  33032  dfon2lem6  33035  dfon2lem7  33036  dfon2lem8  33037  dfon2  33039  axextbdist  33047  distel  33050  axextndbi  33051  fness  33699  fneref  33700  bj-elequ12  34014  bj-axc14nf  34181  bj-bm1.3ii  34359  matunitlindflem1  34890  prtlem13  36006  prtlem15  36013  prtlem17  36014  dveel2ALT  36077  ax12el  36080  aomclem8  39668  elintima  40005  mnuprdlem3  40617  axc11next  40745