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

Theorem elequ2 1649
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 1451 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax-14 1451 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1642 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 128 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1384  ax-ie2 1429  ax-8 1441  ax-14 1451  ax-17 1465  ax-i9 1469
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  elsb4  1902  dveel2  1946  axext3  2072  axext4  2073  bm1.1  2074  eleq2w  2150  bm1.3ii  3966  nalset  3975  zfun  4270  fv3  5341  tfrlemisucaccv  6104  tfr1onlemsucaccv  6120  tfrcllemsucaccv  6133  bdsepnft  12044  bdsepnfALT  12046  bdbm1.3ii  12048  bj-nalset  12052  bj-nnelirr  12114  strcollnft  12145  strcollnfALT  12147  nninfalllem1  12165  nninfsellemeq  12172  nninfsellemqall  12173  nninfsellemeqinf  12174  nninfomni  12177
  Copyright terms: Public domain W3C validator