Theorem elequ1 2151

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 2150	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))
2		ax8 2150	. . 3 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
3	2	equcoms 2052	. 2 ⊢ (𝑥 = 𝑦 → (𝑦 ∈ 𝑧 → 𝑥 ∈ 𝑧))
4	1, 3	impbid 215	1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by:  elsb1  2152  cleljust  2153  elequ12  2162  ru0  2163  ax12wdemo  2171  cleljustALT  2393  cleljustALT2  2394  dveel1  2490  axc14  2492  sbralie  3338  sbralieOLD  3340  unissb  4900  dftr2c  5214  axsepgfromrep  5246  exnelv  5266  nalsetOLD  5268  zfpow  5327  dtruALT2  5331  el.OLD  5406  zfun  7753  tz7.48lemOLD  8455  coflton  8684  pssnn  9188  unxpdomlem1  9251  elirrv  9595  elirrvOLD  9596  zfinf  9644  aceq1  10200  aceq0  10201  aceq2  10202  dfac3  10204  dfac5lem2  10207  dfac5lem3  10208  dfac2a  10212  kmlem4  10236  zfac  10542  nd1  10676  axextnd  10680  axrepndlem1  10681  axrepndlem2  10682  axunndlem1  10684  axunnd  10685  axpowndlem2  10687  axpowndlem3  10688  axpowndlem4  10689  axregndlem1  10691  axregnd  10693  zfcndun  10704  zfcndpow  10705  zfcndinf  10707  zfcndac  10708  fpwwe2lem11  10730  axgroth3  10920  axgroth4  10921  nqereu  11018  mdetunilem9  22941  madugsum  22964  neiptopnei  23456  2ndc1stc  23775  nrmr0reg  24074  alexsubALTlem4  24375  xrsmopn  25138  itg2cn  26090  itgcn  26171  sqff1o  27515  dya2iocuni  34962  bnj849  35602  axprALT2  35787  fineqvrep  35839  axreg  35852  axsepg2  35865  axsepg4  35868  axnulg  35870  axpowg  35871  erdsze  36054  untsucf  36568  untangtr  36572  dfon2lem3  36640  dfon2lem6  36643  dfon2lem7  36644  dfon2  36647  axextdist  36654  distel  36658  nmulprop  37032  neibastop2lem  37241  axtco1  37354  axtco2  37355  axtco1from2  37356  axtcond  37359  axuntco  37360  axnulregtco  37361  regsfromregtco  37419  regsfromsetind  37420  mh-prprimbi  37424  mh-unprimbi  37425  mh-regprimbi  37426  mh-infprim2bi  37428  bj-nfeel2  37859  bj-axseprep  38083  prtlem5  40011  prtlem13  40019  prtlem16  40020  ax12el  40093  pw2f1ocnv  44138  aomclem8  44157  onsupmaxb  44335  grumnud  45364  dfnbgr6  49049  lcosslsp  49644