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

Theorem elequ2 1674
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 1475 . 2  |-  ( x  =  y  ->  (
z  e.  x  -> 
z  e.  y ) )
2 ax-14 1475 . . 3  |-  ( y  =  x  ->  (
z  e.  y  -> 
z  e.  x ) )
32equcoms 1667 . 2  |-  ( x  =  y  ->  (
z  e.  y  -> 
z  e.  x ) )
41, 3impbid 128 1  |-  ( x  =  y  ->  (
z  e.  x  <->  z  e.  y ) )
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 1408  ax-ie2 1453  ax-8 1465  ax-14 1475  ax-17 1489  ax-i9 1493
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  elsb4  1928  dveel2  1972  axext3  2098  axext4  2099  bm1.1  2100  eleq2w  2177  bm1.3ii  4017  nalset  4026  zfun  4324  fv3  5410  tfrlemisucaccv  6188  tfr1onlemsucaccv  6204  tfrcllemsucaccv  6217  acfun  7027  ccfunen  7043  bdsepnft  12919  bdsepnfALT  12921  bdbm1.3ii  12923  bj-nalset  12927  bj-nnelirr  12985  strcollnft  13016  strcollnfALT  13018  nninfalllem1  13037  nninfsellemeq  13044  nninfsellemqall  13045  nninfsellemeqinf  13046  nninfomni  13049
  Copyright terms: Public domain W3C validator