Theorem elequ2 2124

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 2123	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2123	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2020	. 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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119

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

This theorem is referenced by:  elequ2g  2125  elsb2  2126  elequ12  2127  ax12wdemo  2136  dveel2  2460  axextg  2703  axextmo  2705  eleq2w  2812  nfcvf  2918  sbralie  3323  unissb  4899  dftr2c  5212  axrep1  5230  axreplem  5231  axrep4OLD  5236  axsepg  5247  bm1.3iiOLD  5252  nalset  5263  fv3  6858  zfun  7692  tz7.48lem  8386  coflton  8612  aceq1  10046  aceq0  10047  aceq2  10048  dfac2a  10059  kmlem4  10083  axdc3lem2  10380  zfac  10389  nd2  10517  nd3  10518  axrepndlem2  10522  axunndlem1  10524  axunnd  10525  axpowndlem2  10527  axpowndlem3  10528  axpowndlem4  10529  axpownd  10530  axregndlem2  10532  axregnd  10533  axinfndlem1  10534  axacndlem5  10540  zfcndrep  10543  zfcndun  10544  zfcndac  10548  axgroth4  10761  nqereu  10858  mdetunilem9  22483  neiptopnei  22995  2ndc1stc  23314  restlly  23346  kqt0lem  23599  regr1lem2  23603  nrmr0reg  23612  hauspwpwf1  23850  constrcbvlem  33718  dya2iocuni  34247  axsepg2  35045  axsepg2ALT  35046  axnulg  35055  erdsze  35162  untsucf  35670  untangtr  35674  dfon2lem3  35746  dfon2lem6  35749  dfon2lem7  35750  dfon2lem8  35751  dfon2  35753  axextbdist  35761  distel  35764  axextndbi  35765  fness  36310  fneref  36311  bj-axc14nf  36816  bj-bm1.3ii  37025  matunitlindflem1  37583  prtlem13  38834  prtlem15  38841  prtlem17  38842  dveel2ALT  38905  ax12el  38908  aomclem8  43023  unielss  43180  elintima  43615  mnuprdlem3  44236  ismnushort  44263  axc11next  44368  setcthin  49427