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

Theorem eleq1w 2176
Description: Weaker version of eleq1 2178 (but more general than elequ1 1673) not depending on ax-ext 2097 nor df-cleq 2108. (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 1672 . . . 4  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
21anbi1d 458 . . 3  |-  ( x  =  y  ->  (
( z  =  x  /\  z  e.  A
)  <->  ( z  =  y  /\  z  e.  A ) ) )
32exbidv 1779 . 2  |-  ( x  =  y  ->  ( E. z ( z  =  x  /\  z  e.  A )  <->  E. z
( z  =  y  /\  z  e.  A
) ) )
4 df-clel 2111 . 2  |-  ( x  e.  A  <->  E. z
( z  =  x  /\  z  e.  A
) )
5 df-clel 2111 . 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 1451    e. wcel 1463
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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-clel 2111
This theorem is referenced by:  clelsb3f  2260  dfdif3  3154  dfss4st  3277  abn0m  3356  r19.2m  3417  cbvmptf  3990  iinexgm  4047  xpiindim  4644  cnviinm  5048  iinerm  6467  ixpiinm  6584  ixpsnf1o  6596  mapsnen  6671  enumctlemm  6965  exmidomni  6980  fodjum  6984  suplocexprlemmu  7490  suplocsr  7581  axpre-suploc  7674  iseqf1olemqk  10218  seq3f1olemqsum  10224  summodclem2  11102  summodc  11103  zsumdc  11104  fsum3  11107  isumz  11109  isumss  11111  fisumss  11112  isumss2  11113  fsum3cvg2  11114  fsumsersdc  11115  fsum3ser  11117  fsumsplit  11127  fsumsplitf  11128  isumlessdc  11216  neipsm  12229  dedekindeulemub  12671  dedekindeulemloc  12672  dedekindeulemlub  12673  suplociccex  12678  dedekindicclemub  12680  dedekindicclemloc  12681  dedekindicclemlub  12682  limcimo  12709  nninfalllemn  13036
  Copyright terms: Public domain W3C validator