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  3315  unissb  4890  dftr2c  5202  axrep1  5219  axreplem  5220  axrep4OLD  5225  axsepg  5236  bm1.3iiOLD  5241  nalset  5252  fv3  6840  zfun  7672  tz7.48lem  8363  coflton  8589  aceq1  10011  aceq0  10012  aceq2  10013  dfac2a  10024  kmlem4  10048  axdc3lem2  10345  zfac  10354  nd2  10482  nd3  10483  axrepndlem2  10487  axunndlem1  10489  axunnd  10490  axpowndlem2  10492  axpowndlem3  10493  axpowndlem4  10494  axpownd  10495  axregndlem2  10497  axregnd  10498  axinfndlem1  10499  axacndlem5  10505  zfcndrep  10508  zfcndun  10509  zfcndac  10513  axgroth4  10726  nqereu  10823  mdetunilem9  22505  neiptopnei  23017  2ndc1stc  23336  restlly  23368  kqt0lem  23621  regr1lem2  23625  nrmr0reg  23634  hauspwpwf1  23872  constrcbvlem  33722  dya2iocuni  34251  axsepg2  35049  axsepg2ALT  35050  axnulg  35059  erdsze  35179  untsucf  35687  untangtr  35691  dfon2lem3  35763  dfon2lem6  35766  dfon2lem7  35767  dfon2lem8  35768  dfon2  35770  axextbdist  35778  distel  35781  axextndbi  35782  fness  36327  fneref  36328  bj-axc14nf  36833  bj-bm1.3ii  37042  matunitlindflem1  37600  prtlem13  38851  prtlem15  38858  prtlem17  38859  dveel2ALT  38922  ax12el  38925  aomclem8  43038  unielss  43195  elintima  43630  mnuprdlem3  44251  ismnushort  44278  axc11next  44383  setcthin  49454