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

Theorem eleq1w 2148
Description: Weaker version of eleq1 2150 (but more general than elequ1 1647) not depending on ax-ext 2070 nor df-cleq 2081. (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 1646 . . . 4  |-  ( x  =  y  ->  (
z  =  x  <->  z  =  y ) )
21anbi1d 453 . . 3  |-  ( x  =  y  ->  (
( z  =  x  /\  z  e.  A
)  <->  ( z  =  y  /\  z  e.  A ) ) )
32exbidv 1753 . 2  |-  ( x  =  y  ->  ( E. z ( z  =  x  /\  z  e.  A )  <->  E. z
( z  =  y  /\  z  e.  A
) ) )
4 df-clel 2084 . 2  |-  ( x  e.  A  <->  E. z
( z  =  x  /\  z  e.  A
) )
5 df-clel 2084 . 2  |-  ( y  e.  A  <->  E. z
( z  =  y  /\  z  e.  A
) )
63, 4, 53bitr4g 221 1  |-  ( x  =  y  ->  (
x  e.  A  <->  y  e.  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103   E.wex 1426    e. wcel 1438
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-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-clel 2084
This theorem is referenced by:  clelsb3f  2232  dfdif3  3110  dfss4st  3232  abn0m  3308  cbvmptf  3932  mapsnen  6526  exmidomni  6796  fodjuomnilemm  6799  iseqf1olemqk  9919  seq3f1olemqsum  9925  isummolem2  10768  isummo  10769  zisum  10770  fisum  10774  isumz  10777  isumss  10779  fisumss  10780  isumss2  10781  fisumcvg2  10782  fsum3cvg2  10783  fisumsers  10784  fisumser  10786  fsumsplit  10797  fsumsplitf  10798  isumlessdc  10886  nninfalllemn  11853
  Copyright terms: Public domain W3C validator