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  15756  bdsepnfALT  15758  bdbm1.3ii  15760  bj-nalset  15764  bj-nnelirr  15822  nninfalllem1  15878  nninfsellemeq  15884  nninfsellemqall  15885  nninfsellemeqinf  15886  nninfomni  15889
  Copyright terms: Public domain W3C validator