Theorem elequ2 1991

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 1990	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 1990	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 1934	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
4	1, 3	impbid 201	1 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦))

Syntax hints:   → wi 4   ↔ wb 195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696

This theorem is referenced by:  ax12wdemo  1999  dveel2  2359  elsb4  2423  axext3  2592  axext3ALT  2593  axext4  2594  bm1.1  2595  axrep1  4700  axrep2  4701  axrep3  4702  axrep4  4703  bm1.3ii  4712  nalset  4723  fv3  6116  zfun  6848  tz7.48lem  7423  aceq0  8824  dfac2a  8835  axdc3lem2  9156  zfac  9165  nd2  9289  nd3  9290  axrepndlem2  9294  axunndlem1  9296  axunnd  9297  axpowndlem2  9299  axpowndlem3  9300  axpowndlem4  9301  axpownd  9302  axregndlem2  9304  axregnd  9305  axinfndlem1  9306  axacndlem5  9312  zfcndrep  9315  zfcndun  9316  zfcndac  9320  axgroth4  9533  nqereu  9630  mdetunilem9  20245  neiptopnei  20746  2ndc1stc  21064  kqt0lem  21349  regr1lem2  21353  nrmr0reg  21362  hauspwpwf1  21601  dya2iocuni  29672  erdsze  30438  untsucf  30841  untangtr  30845  dfon2lem3  30934  dfon2lem6  30937  dfon2lem7  30938  dfon2lem8  30939  dfon2  30941  axext4dist  30950  distel  30953  axextndbi  30954  fness  31514  fneref  31515  bj-elequ2g  31853  bj-elequ12  31855  bj-axext3  31957  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axrep4  31979  bj-nalset  31982  bj-eleq2w  32041  bj-axsep2  32113  matunitlindflem1  32575  prtlem13  33171  prtlem15  33178  prtlem17  33179  dveel2ALT  33242  ax12el  33245  aomclem8  36649  elintima  36964  axc11next  37629