Theorem elequ2 2121

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 2120	. 2 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝑥 → 𝑧 ∈ 𝑦))
2		ax9 2120	. . 3 ⊢ (𝑦 = 𝑥 → (𝑧 ∈ 𝑦 → 𝑧 ∈ 𝑥))
3	2	equcoms 2017	. 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 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116

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

This theorem is referenced by:  elequ2g  2122  elsb2  2123  elequ12  2124  ax12wdemo  2133  dveel2  2465  axextg  2708  axextmo  2710  eleq2w  2823  nfcvf  2930  unissb  4944  dftr2c  5268  axrep1  5286  axreplem  5287  axrep4OLD  5292  axsepg  5303  bm1.3iiOLD  5308  nalset  5319  fv3  6925  zfun  7755  tz7.48lem  8480  coflton  8708  aceq1  10155  aceq0  10156  aceq2  10157  dfac2a  10168  kmlem4  10192  axdc3lem2  10489  zfac  10498  nd2  10626  nd3  10627  axrepndlem2  10631  axunndlem1  10633  axunnd  10634  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axpownd  10639  axregndlem2  10641  axregnd  10642  axinfndlem1  10643  axacndlem5  10649  zfcndrep  10652  zfcndun  10653  zfcndac  10657  axgroth4  10870  nqereu  10967  mdetunilem9  22642  neiptopnei  23156  2ndc1stc  23475  restlly  23507  kqt0lem  23760  regr1lem2  23764  nrmr0reg  23773  hauspwpwf1  24011  dya2iocuni  34265  axsepg2  35075  axsepg2ALT  35076  axnulg  35085  erdsze  35187  untsucf  35690  untangtr  35694  dfon2lem3  35767  dfon2lem6  35770  dfon2lem7  35771  dfon2lem8  35772  dfon2  35774  axextbdist  35782  distel  35785  axextndbi  35786  fness  36332  fneref  36333  bj-axc14nf  36838  bj-bm1.3ii  37047  matunitlindflem1  37603  prtlem13  38850  prtlem15  38857  prtlem17  38858  dveel2ALT  38921  ax12el  38924  aomclem8  43050  unielss  43207  elintima  43643  mnuprdlem3  44270  ismnushort  44297  axc11next  44402  setcthin  48856