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

Theorem elequ2 2130
 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 2128 . 2 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
2 ax-14 2128 . . 3 (𝑦 = 𝑥 → (𝑧𝑦𝑧𝑥))
32equcoms 1685 . 2 (𝑥 = 𝑦 → (𝑧𝑦𝑧𝑥))
41, 3impbid 128 1 (𝑥 = 𝑦 → (𝑧𝑥𝑧𝑦))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie2 1471  ax-8 1481  ax-17 1503  ax-i9 1507  ax-14 2128 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  elsb4  2133  dveel2  2135  axext3  2137  axext4  2138  bm1.1  2139  eleq2w  2216  bm1.3ii  4081  nalset  4090  zfun  4389  fv3  5484  tfrlemisucaccv  6262  tfr1onlemsucaccv  6278  tfrcllemsucaccv  6291  acfun  7121  ccfunen  7163  cc1  7164  bdsepnft  13400  bdsepnfALT  13402  bdbm1.3ii  13404  bj-nalset  13408  bj-nnelirr  13466  nninfalllem1  13521  nninfsellemeq  13527  nninfsellemqall  13528  nninfsellemeqinf  13529  nninfomni  13532
 Copyright terms: Public domain W3C validator