Theorem elequ2 2126

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 2125	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2125	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2027	. 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 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782

This theorem is referenced by:  elsb4  2127  elequ2g  2128  ax12wdemo  2136  dveel2  2474  axextg  2772  axextmo  2774  eleq2w  2873  nfcvf  2981  axrep1  5155  axreplem  5156  axrep4  5159  axsepg  5168  bm1.3ii  5170  nalset  5181  fv3  6663  zfun  7442  tz7.48lem  8060  aceq1  9528  aceq0  9529  aceq2  9530  dfac2a  9540  kmlem4  9564  axdc3lem2  9862  zfac  9871  nd2  9999  nd3  10000  axrepndlem2  10004  axunndlem1  10006  axunnd  10007  axpowndlem2  10009  axpowndlem3  10010  axpowndlem4  10011  axpownd  10012  axregndlem2  10014  axregnd  10015  axinfndlem1  10016  axacndlem5  10022  zfcndrep  10025  zfcndun  10026  zfcndac  10030  axgroth4  10243  nqereu  10340  elnpi  10399  mdetunilem9  21225  neiptopnei  21737  2ndc1stc  22056  restlly  22088  kqt0lem  22341  regr1lem2  22345  nrmr0reg  22354  hauspwpwf1  22592  dya2iocuni  31651  erdsze  32562  untsucf  33049  untangtr  33053  dfon2lem3  33143  dfon2lem6  33146  dfon2lem7  33147  dfon2lem8  33148  dfon2  33150  axextbdist  33158  distel  33161  axextndbi  33162  fness  33810  fneref  33811  bj-elequ12  34125  bj-axc14nf  34294  bj-bm1.3ii  34481  matunitlindflem1  35053  prtlem13  36164  prtlem15  36171  prtlem17  36172  dveel2ALT  36235  ax12el  36238  aomclem8  40005  elintima  40354  mnuprdlem3  40982  axc11next  41110