Theorem elequ1 2118

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 2117	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2117	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2021	. 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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113

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

This theorem is referenced by:  elsb1  2119  cleljust  2120  elequ12  2129  ru0  2130  ax12wdemo  2138  cleljustALT  2364  cleljustALT2  2365  dveel1  2461  axc14  2463  sbralie  3318  sbralieOLD  3320  unissb  4891  dftr2c  5201  axsepgfromrep  5232  nalset  5251  zfpow  5304  dtruALT2  5308  el  5380  zfun  7669  tz7.48lem  8360  coflton  8586  pssnn  9078  unxpdomlem1  9140  elirrv  9483  zfinf  9529  aceq1  10005  aceq0  10006  aceq2  10007  dfac3  10009  dfac5lem2  10012  dfac5lem3  10013  dfac2a  10018  kmlem4  10042  zfac  10348  nd1  10475  axextnd  10479  axrepndlem1  10480  axrepndlem2  10481  axunndlem1  10483  axunnd  10484  axpowndlem2  10486  axpowndlem3  10487  axpowndlem4  10488  axregndlem1  10490  axregnd  10492  zfcndun  10503  zfcndpow  10504  zfcndinf  10506  zfcndac  10507  fpwwe2lem11  10529  axgroth3  10719  axgroth4  10720  nqereu  10817  mdetunilem9  22533  madugsum  22556  neiptopnei  23045  2ndc1stc  23364  nrmr0reg  23662  alexsubALTlem4  23963  xrsmopn  24726  itg2cn  25689  itgcn  25771  sqff1o  27117  dya2iocuni  34291  bnj849  34932  axnulg  35110  axreg  35113  fineqvrep  35125  erdsze  35234  untsucf  35742  untangtr  35746  dfon2lem3  35818  dfon2lem6  35821  dfon2lem7  35822  dfon2  35825  axextdist  35832  distel  35836  neibastop2lem  36393  bj-nfeel2  36887  prtlem5  38898  prtlem13  38906  prtlem16  38907  ax12el  38980  pw2f1ocnv  43069  aomclem8  43093  onsupmaxb  43271  grumnud  44318  dfnbgr6  47887  lcosslsp  48469