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  22540  neiptopnei  23052  2ndc1stc  23371  restlly  23403  kqt0lem  23656  regr1lem2  23660  nrmr0reg  23669  hauspwpwf1  23907  constrcbvlem  33738  dya2iocuni  34267  axsepg2  35065  axsepg2ALT  35066  axnulg  35075  erdsze  35182  untsucf  35690  untangtr  35694  dfon2lem3  35766  dfon2lem6  35769  dfon2lem7  35770  dfon2lem8  35771  dfon2  35773  axextbdist  35781  distel  35784  axextndbi  35785  fness  36330  fneref  36331  bj-axc14nf  36836  bj-bm1.3ii  37045  matunitlindflem1  37603  prtlem13  38854  prtlem15  38861  prtlem17  38862  dveel2ALT  38925  ax12el  38928  aomclem8  43043  unielss  43200  elintima  43635  mnuprdlem3  44256  ismnushort  44283  axc11next  44388  setcthin  49447