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

Theorem eleq1w 2178
Description: Weaker version of eleq1 2180 (but more general than elequ1 1675) not depending on ax-ext 2099 nor df-cleq 2110. (Contributed by BJ, 24-Jun-2019.)
Assertion
Ref Expression
eleq1w  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )

Proof of Theorem eleq1w
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 equequ2 1674 . . . 4  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
21anbi1d 460 . . 3  |-  ( x  =  y  ->  (
( z  =  x  /\  z  e.  A
)  <->  ( z  =  y  /\  z  e.  A ) ) )
32exbidv 1781 . 2  |-  ( x  =  y  ->  ( E. z ( z  =  x  /\  z  e.  A )  <->  E. z
( z  =  y  /\  z  e.  A
) ) )
4 df-clel 2113 . 2  |-  ( x  e.  A  <->  E. z
( z  =  x  /\  z  e.  A
) )
5 df-clel 2113 . 2  |-  ( y  e.  A  <->  E. z
( z  =  y  /\  z  e.  A
) )
63, 4, 53bitr4g 222 1  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   E.wex 1453    e. wcel 1465
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499
This theorem depends on definitions:  df-bi 116  df-clel 2113
This theorem is referenced by:  clelsb3f  2262  dfdif3  3156  dfss4st  3279  abn0m  3358  r19.2m  3419  cbvmptf  3992  iinexgm  4049  xpiindim  4646  cnviinm  5050  iinerm  6469  ixpiinm  6586  ixpsnf1o  6598  mapsnen  6673  enumctlemm  6967  exmidomni  6982  fodjum  6986  suplocexprlemmu  7494  suplocsr  7585  axpre-suploc  7678  iseqf1olemqk  10222  seq3f1olemqsum  10228  summodclem2  11106  summodc  11107  zsumdc  11108  fsum3  11111  isumz  11113  isumss  11115  fisumss  11116  isumss2  11117  fsum3cvg2  11118  fsumsersdc  11119  fsum3ser  11121  fsumsplit  11131  fsumsplitf  11132  isumlessdc  11220  neipsm  12234  dedekindeulemub  12676  dedekindeulemloc  12677  dedekindeulemlub  12678  suplociccex  12683  dedekindicclemub  12685  dedekindicclemloc  12686  dedekindicclemlub  12687  limcimo  12714  nninfalllemn  13098
  Copyright terms: Public domain W3C validator