ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elequ2 GIF version

Theorem elequ2 1648
Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
elequ2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))

Proof of Theorem elequ2
StepHypRef Expression
1 ax-14 1450 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax-14 1450 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1641 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 127 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383  ax-ie2 1428  ax-8 1440  ax-14 1450  ax-17 1464  ax-i9 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  elsb4  1901  dveel2  1945  axext3  2071  axext4  2072  bm1.1  2073  eleq2w  2149  bm1.3ii  3952  nalset  3961  zfun  4252  fv3  5312  tfrlemisucaccv  6072  tfr1onlemsucaccv  6088  tfrcllemsucaccv  6101  bdsepnft  11424  bdsepnfALT  11426  bdbm1.3ii  11428  bj-nalset  11432  bj-nnelirr  11494  strcollnft  11525  strcollnfALT  11527  nninfalllem1  11545  nninfsellemeq  11552  nninfsellemqall  11553  nninfsellemeqinf  11554  nninfomni  11557
  Copyright terms: Public domain W3C validator