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

Theorem elequ2 1648
Description: An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
elequ2  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )

Proof of Theorem elequ2
StepHypRef Expression
1 ax-14 1450 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1450 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1641 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 127 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
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  11435  bdsepnfALT  11437  bdbm1.3ii  11439  bj-nalset  11443  bj-nnelirr  11505  strcollnft  11536  strcollnfALT  11538  nninfalllem1  11556  nninfsellemeq  11563  nninfsellemqall  11564  nninfsellemeqinf  11565  nninfomni  11568
  Copyright terms: Public domain W3C validator