Theorem elequ1 2113

Description: An identity law for the non-logical predicate. (Contributed by NM, 30-Jun-1993.)

Assertion

Ref	Expression
elequ1	⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

Proof of Theorem elequ1

Step	Hyp	Ref	Expression
1		ax8 2112	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2112	. . 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-8 2108

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

This theorem is referenced by:  elsb1  2114  cleljust  2115  elequ12  2124  ru0  2125  ax12wdemo  2133  cleljustALT  2365  cleljustALT2  2366  dveel1  2464  axc14  2466  sbralie  3356  unissb  4944  dftr2c  5268  axsepgfromrep  5300  nalset  5319  zfpow  5372  dtruALT2  5376  el  5448  dtruOLD  5452  zfun  7755  tz7.48lem  8480  coflton  8708  pssnn  9207  unxpdomlem1  9284  zfinf  9677  aceq1  10155  aceq0  10156  aceq2  10157  dfac3  10159  dfac5lem2  10162  dfac5lem3  10163  dfac2a  10168  kmlem4  10192  zfac  10498  nd1  10625  axextnd  10629  axrepndlem1  10630  axrepndlem2  10631  axunndlem1  10633  axunnd  10634  axpowndlem2  10636  axpowndlem3  10637  axpowndlem4  10638  axregndlem1  10640  axregnd  10642  zfcndun  10653  zfcndpow  10654  zfcndinf  10656  zfcndac  10657  fpwwe2lem11  10679  axgroth3  10869  axgroth4  10870  nqereu  10967  mdetunilem9  22642  madugsum  22665  neiptopnei  23156  2ndc1stc  23475  nrmr0reg  23773  alexsubALTlem4  24074  xrsmopn  24848  itg2cn  25813  itgcn  25895  sqff1o  27240  dya2iocuni  34265  bnj849  34918  axnulg  35085  fineqvrep  35088  erdsze  35187  untsucf  35690  untangtr  35694  dfon2lem3  35767  dfon2lem6  35770  dfon2lem7  35771  dfon2  35774  axextdist  35781  distel  35785  neibastop2lem  36343  bj-nfeel2  36837  prtlem5  38842  prtlem13  38850  prtlem16  38851  ax12el  38924  pw2f1ocnv  43026  aomclem8  43050  onsupmaxb  43228  grumnud  44282  dfnbgr6  47781  lcosslsp  48284