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

Theorem elequ2 2153
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 2151 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 2151 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1708 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 129 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530  ax-14 2151
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  elsb2  2156  dveel2  2158  axext3  2160  axext4  2161  bm1.1  2162  eleq2w  2239  bm1.3ii  4124  nalset  4133  zfun  4434  fv3  5538  tfrlemisucaccv  6325  tfr1onlemsucaccv  6341  tfrcllemsucaccv  6354  acfun  7205  ccfunen  7262  cc1  7263  bdsepnft  14521  bdsepnfALT  14523  bdbm1.3ii  14525  bj-nalset  14529  bj-nnelirr  14587  nninfalllem1  14639  nninfsellemeq  14645  nninfsellemqall  14646  nninfsellemeqinf  14647  nninfomni  14650
  Copyright terms: Public domain W3C validator