Theorem elequ1 2150

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

Syntax hints:   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  elsb1  2151  cleljust  2152  elequ12  2161  ru0  2162  ax12wdemo  2170  cleljustALT  2396  cleljustALT2  2397  dveel1  2493  axc14  2495  sbralie  3342  sbralieOLD  3344  unissb  4907  dftr2c  5222  axsepgfromrep  5256  exnelv  5277  nalsetOLD  5279  zfpow  5339  dtruALT2  5343  elOLD  5422  zfun  7735  tz7.48lem  8429  coflton  8658  pssnn  9154  unxpdomlem1  9217  elirrv  9560  elirrvOLD  9561  zfinf  9609  aceq1  10102  aceq0  10103  aceq2  10104  dfac3  10106  dfac5lem2  10109  dfac5lem3  10110  dfac2a  10114  kmlem4  10138  zfac  10445  nd1  10573  axextnd  10577  axrepndlem1  10578  axrepndlem2  10579  axunndlem1  10581  axunnd  10582  axpowndlem2  10584  axpowndlem3  10585  axpowndlem4  10586  axregndlem1  10588  axregnd  10590  zfcndun  10601  zfcndpow  10602  zfcndinf  10604  zfcndac  10605  fpwwe2lem11  10627  axgroth3  10817  axgroth4  10818  nqereu  10915  mdetunilem9  22758  madugsum  22781  neiptopnei  23270  2ndc1stc  23589  nrmr0reg  23887  alexsubALTlem4  24188  xrsmopn  24951  itg2cn  25903  itgcn  25985  sqff1o  27327  dya2iocuni  34654  bnj849  35294  axprALT2  35484  fineqvrep  35508  axreg  35521  axsepg2  35534  axsepg4  35537  axnulg  35539  axpowg  35540  erdsze  35675  untsucf  36183  untangtr  36187  dfon2lem3  36256  dfon2lem6  36259  dfon2lem7  36260  dfon2  36263  axextdist  36270  distel  36274  nmulprop  36663  neibastop2lem  36852  axtco1  36965  axtco2  36966  axtco1from2  36967  axtcond  36970  axuntco  36971  axnulregtco  36972  regsfromregtco  37030  regsfromsetind  37031  mh-prprimbi  37035  mh-unprimbi  37036  mh-regprimbi  37037  mh-infprim2bi  37039  bj-nfeel2  37470  bj-axseprep  37692  prtlem5  39615  prtlem13  39623  prtlem16  39624  ax12el  39697  pw2f1ocnv  43747  aomclem8  43771  onsupmaxb  43949  grumnud  44979  dfnbgr6  48605  lcosslsp  49201