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  3326  unissb  4903  dftr2c  5217  axrep1  5235  axreplem  5236  axrep4OLD  5241  axsepg  5252  bm1.3iiOLD  5257  nalset  5268  fv3  6876  zfun  7712  tz7.48lem  8409  coflton  8635  aceq1  10070  aceq0  10071  aceq2  10072  dfac2a  10083  kmlem4  10107  axdc3lem2  10404  zfac  10413  nd2  10541  nd3  10542  axrepndlem2  10546  axunndlem1  10548  axunnd  10549  axpowndlem2  10551  axpowndlem3  10552  axpowndlem4  10553  axpownd  10554  axregndlem2  10556  axregnd  10557  axinfndlem1  10558  axacndlem5  10564  zfcndrep  10567  zfcndun  10568  zfcndac  10572  axgroth4  10785  nqereu  10882  mdetunilem9  22507  neiptopnei  23019  2ndc1stc  23338  restlly  23370  kqt0lem  23623  regr1lem2  23627  nrmr0reg  23636  hauspwpwf1  23874  constrcbvlem  33745  dya2iocuni  34274  axsepg2  35072  axsepg2ALT  35073  axnulg  35082  erdsze  35189  untsucf  35697  untangtr  35701  dfon2lem3  35773  dfon2lem6  35776  dfon2lem7  35777  dfon2lem8  35778  dfon2  35780  axextbdist  35788  distel  35791  axextndbi  35792  fness  36337  fneref  36338  bj-axc14nf  36843  bj-bm1.3ii  37052  matunitlindflem1  37610  prtlem13  38861  prtlem15  38868  prtlem17  38869  dveel2ALT  38932  ax12el  38935  aomclem8  43050  unielss  43207  elintima  43642  mnuprdlem3  44263  ismnushort  44290  axc11next  44395  setcthin  49454