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

Theorem eleq2 2176
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 2107 . . . . . 6  |-  ( A  =  B  <->  A. x
( x  e.  A  <->  x  e.  B ) )
21biimpi 119 . . . . 5  |-  ( A  =  B  ->  A. x
( x  e.  A  <->  x  e.  B ) )
3219.21bi 1518 . . . 4  |-  ( A  =  B  ->  (
x  e.  A  <->  x  e.  B ) )
43anbi2d 457 . . 3  |-  ( A  =  B  ->  (
( x  =  C  /\  x  e.  A
)  <->  ( x  =  C  /\  x  e.  B ) ) )
54exbidv 1777 . 2  |-  ( A  =  B  ->  ( E. x ( x  =  C  /\  x  e.  A )  <->  E. x
( x  =  C  /\  x  e.  B
) ) )
6 df-clel 2109 . 2  |-  ( C  e.  A  <->  E. x
( x  =  C  /\  x  e.  A
) )
7 df-clel 2109 . 2  |-  ( C  e.  B  <->  E. x
( x  =  C  /\  x  e.  B
) )
85, 6, 73bitr4g 222 1  |-  ( A  =  B  ->  ( C  e.  A  <->  C  e.  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104   A.wal 1310    = wceq 1312   E.wex 1449    e. wcel 1461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-4 1468  ax-17 1487  ax-ial 1495  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-cleq 2106  df-clel 2109
This theorem is referenced by:  eleq12  2177  eleq2i  2179  eleq2d  2182  nelneq2  2214  clelsb4  2218  dvelimdc  2273  nelne1  2370  neleq2  2380  raleqf  2594  rexeqf  2595  reueq1f  2596  rmoeq1f  2597  rabeqf  2645  clel3g  2787  clel4  2789  sbcbi2  2925  sbcel2gv  2938  sbnfc2  3024  difeq2  3152  uneq1  3187  ineq1  3234  n0i  3332  disjel  3381  exsnrex  3530  sneqr  3651  preqr1g  3657  preqr1  3659  preq12b  3661  prel12  3662  elunii  3705  eluniab  3712  ssuni  3722  elinti  3744  elintab  3746  intss1  3750  intmin  3755  intab  3764  iineq2  3794  dfiin2g  3810  breq  3895  axsep2  4005  zfauscl  4006  inuni  4038  exmidexmid  4078  exmid01  4079  exmidundif  4087  exmidundifim  4088  rext  4095  intid  4104  mss  4106  opth1  4116  opeqex  4129  frforeq3  4227  frirrg  4230  limeq  4257  nsuceq0g  4298  suctr  4301  snnex  4327  uniuni  4330  iunpw  4359  ordtriexmidlem  4393  ordtriexmidlem2  4394  ordtriexmid  4395  ordtri2orexmid  4396  ontr2exmid  4398  ordtri2or2exmidlem  4399  onsucelsucexmidlem  4402  onsucelsucexmid  4403  ordsucunielexmid  4404  regexmidlem1  4406  reg2exmidlema  4407  regexmid  4408  reg2exmid  4409  elirr  4414  en2lp  4427  suc11g  4430  dtruex  4432  ordsoexmid  4435  nlimsucg  4439  onintexmid  4445  reg3exmidlemwe  4451  reg3exmid  4452  peano5  4470  limom  4485  0elnn  4490  nn0eln0  4491  nnregexmid  4492  xpeq1  4511  xpeq2  4512  opthprc  4548  xp11m  4933  funopg  5113  dffo4  5520  elunirn  5619  f1oiso  5679  eusvobj2  5712  acexmidlema  5717  acexmidlemb  5718  acexmidlemab  5720  acexmidlem2  5723  mpoeq123  5782  oprssdmm  6021  unielxp  6024  cnvf1o  6074  smoel  6149  tfr0dm  6171  frecabcl  6248  nnsucelsuc  6339  nntri3or  6341  nntri2  6342  nntri3  6345  nndceq  6347  nnmordi  6364  nnaordex  6375  elqsn0m  6449  qsel  6458  mapsn  6536  findcard2s  6735  undifdcss  6762  ctssdclemr  6947  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  exmidaclem  7009  elni2  7064  addnidpig  7086  elinp  7224  pitonn  7577  peano1nnnn  7581  peano2nnnn  7582  peano5nnnn  7621  sup3exmid  8619  peano5nni  8627  1nn  8635  peano2nn  8636  dfuzi  9059  uz11  9244  elfzonlteqm1  9874  frec2uzltd  10063  0tonninf  10099  1tonninf  10100  sumeq1  11010  ctiunct  11790  istopg  12003  fiinbas  12053  topbas  12073  epttop  12096  restbasg  12174  icnpimaex  12216  lmcvg  12222  iscnp4  12223  cncnpi  12233  cnconst2  12238  cnptoprest  12244  cnptoprest2  12245  cnpdis  12247  lmss  12251  lmff  12254  txbas  12263  eltx  12264  txcnp  12276  txlm  12284  blssps  12410  blss  12411  blssexps  12412  blssex  12413  neibl  12474  metss  12477  metrest  12489  xmettx  12493  metcnp3  12494  tgioo  12526  tgqioo  12527  bdsep2  12767  bdzfauscl  12771  bj-indeq  12810  bj-nn0suc0  12831  bj-nnelirr  12834  bj-peano4  12836  bj-inf2vnlem2  12852  bj-nn0sucALT  12859  bj-findis  12860  nninfsellemdc  12887  nninfsellemqall  12892
  Copyright terms: Public domain W3C validator