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

Theorem eleq2 2117
Description: Equality implies equivalence of membership. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
eleq2  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )

Proof of Theorem eleq2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfcleq 2050 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 117 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1466 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 445 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1722 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2052 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2052 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 216 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101    <-> wb 102   A.wal 1257    = wceq 1259   E.wex 1397    e. wcel 1409
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049  df-clel 2052
This theorem is referenced by:  eleq12  2118  eleq2i  2120  eleq2d  2123  nelneq2  2155  clelsb4  2159  dvelimdc  2213  nelne1  2310  neleq2  2319  raleqf  2518  rexeqf  2519  reueq1f  2520  rmoeq1f  2521  rabeqf  2567  clel3g  2701  clel4  2703  sbcbi2  2836  sbcel2gv  2849  sbnfc2  2934  difeq2  3084  uneq1  3118  ineq1  3159  n0i  3257  disjel  3302  exsnrex  3441  sneqr  3559  preqr1g  3565  preqr1  3567  preq12b  3569  prel12  3570  elunii  3613  eluniab  3620  ssuni  3630  elinti  3652  elintab  3654  intss1  3658  intmin  3663  intab  3672  iineq2  3702  dfiin2g  3718  breq  3794  axsep2  3904  zfauscl  3905  inuni  3937  rext  3979  intid  3988  mss  3990  opth1  4001  opeqex  4014  frforeq3  4112  frirrg  4115  limeq  4142  nsuceq0g  4183  suctr  4186  snnex  4209  uniuni  4211  iunpw  4239  ordtriexmidlem  4273  ordtriexmidlem2  4274  ordtriexmid  4275  ordtri2orexmid  4276  ontr2exmid  4278  ordtri2or2exmidlem  4279  onsucelsucexmidlem  4282  onsucelsucexmid  4283  ordsucunielexmid  4284  regexmidlem1  4286  reg2exmidlema  4287  regexmid  4288  reg2exmid  4289  elirr  4294  en2lp  4306  suc11g  4309  dtruex  4311  ordsoexmid  4314  nlimsucg  4318  onpsssuc  4323  onintexmid  4325  reg3exmidlemwe  4331  reg3exmid  4332  peano5  4349  limom  4364  0elnn  4368  nn0eln0  4369  nnregexmid  4370  xpeq1  4387  xpeq2  4388  opthprc  4419  xp11m  4787  funopg  4962  dffo4  5343  elunirn  5433  f1oiso  5493  eusvobj2  5526  acexmidlema  5531  acexmidlemb  5532  acexmidlemab  5534  acexmidlem2  5537  mpt2eq123  5592  unielxp  5828  cnvf1o  5874  smoel  5946  tfr0  5968  nnsucelsuc  6101  nntri3or  6103  nntri2  6104  nntri3  6106  nndceq  6108  nnmordi  6120  nnaordex  6131  elqsn0m  6205  qsel  6214  findcard2s  6378  elni2  6470  addnidpig  6492  elinp  6630  pitonn  6982  peano1nnnn  6986  peano2nnnn  6987  peano5nnnn  7024  peano5nni  7993  1nn  8001  peano2nn  8002  dfuzi  8407  uz11  8591  elfzonlteqm1  9168  frec2uzltd  9353  bdsep2  10393  bdzfauscl  10397  bj-indeq  10440  bj-nn0suc0  10462  bj-nnelirr  10465  bj-peano4  10467  bj-inf2vnlem2  10483  bj-nn0sucALT  10490  bj-findis  10491
  Copyright terms: Public domain W3C validator