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 2021	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121

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

This theorem is referenced by:  elequ2g  2127  elsb2  2128  elequ12  2129  ax12wdemo  2138  dveel2  2462  axextg  2705  axextmo  2707  eleq2w  2815  nfcvf  2921  sbralie  3318  unissb  4891  dftr2c  5203  axrep1  5220  axreplem  5221  axrep4OLD  5226  axsepg  5237  bm1.3iiOLD  5242  nalset  5253  fv3  6846  zfun  7675  tz7.48lem  8366  coflton  8592  aceq1  10014  aceq0  10015  aceq2  10016  dfac2a  10027  kmlem4  10051  axdc3lem2  10348  zfac  10357  nd2  10485  nd3  10486  axrepndlem2  10490  axunndlem1  10492  axunnd  10493  axpowndlem2  10495  axpowndlem3  10496  axpowndlem4  10497  axpownd  10498  axregndlem2  10500  axregnd  10501  axinfndlem1  10502  axacndlem5  10508  zfcndrep  10511  zfcndun  10512  zfcndac  10516  axgroth4  10729  nqereu  10826  mdetunilem9  22541  neiptopnei  23053  2ndc1stc  23372  restlly  23404  kqt0lem  23657  regr1lem2  23661  nrmr0reg  23670  hauspwpwf1  23908  constrcbvlem  33775  dya2iocuni  34303  axsepg2  35101  axsepg2ALT  35102  axnulg  35126  erdsze  35253  untsucf  35761  untangtr  35765  dfon2lem3  35834  dfon2lem6  35837  dfon2lem7  35838  dfon2lem8  35839  dfon2  35841  axextbdist  35849  distel  35852  axextndbi  35853  fness  36400  fneref  36401  bj-axc14nf  36906  bj-bm1.3ii  37115  matunitlindflem1  37662  prtlem13  38973  prtlem15  38980  prtlem17  38981  dveel2ALT  39044  ax12el  39047  aomclem8  43159  unielss  43316  elintima  43751  mnuprdlem3  44372  ismnushort  44399  axc11next  44504  setcthin  49571