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

Theorem elequ2 2180
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 2178 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax-14 2178 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1730 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 129 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552  ax-14 2178
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  elsb2  2183  dveel2  2185  axext3  2187  axext4  2188  bm1.1  2189  eleq2w  2266  bm1.3ii  4164  nalset  4173  zfun  4480  fv3  5598  tfrlemisucaccv  6410  tfr1onlemsucaccv  6426  tfrcllemsucaccv  6439  acfun  7318  ccfunen  7375  cc1  7376  nninfinf  10586  bdsepnft  15785  bdsepnfALT  15787  bdbm1.3ii  15789  bj-nalset  15793  bj-nnelirr  15851  nninfalllem1  15907  nninfsellemeq  15913  nninfsellemqall  15914  nninfsellemeqinf  15915  nninfomni  15918
  Copyright terms: Public domain W3C validator