MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eleq12d Unicode version

Theorem eleq12d 2351
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq1d.1  |-  ( ph  ->  A  =  B )
eleq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eleq12d  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3  |-  ( ph  ->  C  =  D )
21eleq2d 2350 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2349 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 244 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684
This theorem is referenced by:  cbvraldva2  2768  cbvrexdva2  2769  cdeqel  2987  ru  2990  sbcel12g  3096  cbvralcsf  3143  cbvreucsf  3145  cbvrabcsf  3146  elvvuni  4750  elrnmpt1  4928  ovmpt2dxf  5973  canth  6294  onnseq  6361  smoeq  6367  smores  6369  smores2  6371  iordsmo  6374  tz7.49  6457  nnaordr  6618  omsmolem  6651  fvixp  6821  cbvixp  6833  mptelixpg  6853  boxcutc  6859  ixpiunwdom  7305  elirr  7312  cantnflt  7373  oemapvali  7386  cantnflem1  7391  cantnf  7395  wemapwe  7400  cnfcom3lem  7406  infxpen  7642  dfac8alem  7656  dfac8clem  7659  ac5num  7663  acni2  7673  numacn  7676  acndom  7678  aceq3lem  7747  dfac5  7755  dfac9  7762  dfac13  7768  cofsmo  7895  cfsmolem  7896  fin2i  7921  isfin2-2  7945  fin23lem27  7954  isfin3ds  7955  fin23lem17  7964  fin23lem39  7976  isf33lem  7992  isf34lem7  8005  isf34lem6  8006  fin1a2lem10  8035  fin1a2lem12  8037  hsmexlem4  8055  axcc2lem  8062  axcc3  8064  domtriomlem  8068  axdc2lem  8074  axdc3lem2  8077  axdc3lem3  8078  axdc3lem4  8079  axdc3  8080  axdc4lem  8081  axcclem  8083  ac6num  8106  ac6c4  8108  iundom2g  8162  smobeth  8208  fpwwe2  8265  pwfseqlem1  8280  pwfseqlem4a  8283  pwfseqlem4  8284  ltapi  8527  ltmpi  8528  eluzadd  10256  fzsubel  10827  fzosubel  10908  axdc4uzlem  11044  smuval  12672  prdsbasprj  13371  xpsfrnel  13465  ismri2dad  13539  mreexd  13544  mreacs  13560  iscat  13574  iscatd  13575  iscatd2  13583  catcocl  13587  catpropd  13612  brssc  13691  issubc  13712  subcidcl  13718  subccocl  13719  isfunc  13738  isfuncd  13739  cofucl  13762  funcres2b  13771  fuciso  13849  yonedalem3  14054  yonffthlem  14056  islat  14153  isclat  14215  isla  14342  ismnd  14369  ismndd  14396  mndpropd  14398  mulgnndir  14589  imasgrp  14611  subg0cl  14629  subginvcl  14630  eqgfval  14665  efgsdm  15039  efgsdmi  15041  efgsrel  15043  efgsp1  15046  efgsres  15047  efgcpbllemb  15064  dprdwd  15246  dprdfcl  15248  ablfaclem3  15322  isdrngd  15537  issrng  15615  issrngd  15626  islmodd  15633  lmodprop2d  15687  islbs  15829  lbsind  15833  lbspropd  15852  islbs2  15907  lbsextlem4  15914  lbsextg  15915  psraddcl  16128  qsssubdrg  16431  zndvds  16503  isphl  16532  isphld  16558  phlpropd  16559  istps  16674  tpspropd  16678  eltpsg  16683  islp  16872  1stcelcls  17187  kgeni  17232  kgencn2  17252  ptpjpre1  17266  elptr2  17269  ptbasin  17272  ptbasfi  17276  ptpjcn  17305  ptpjopn  17306  ptcld  17307  ptcldmpt  17308  ptclsg  17309  ptcnp  17316  prdstps  17323  qtopval  17386  xpstopnlem1  17500  ptcmplem2  17747  ptcmplem3  17748  ptcmplem4  17749  istmd  17757  istgp  17760  tmdgsum  17778  tsmssub  17831  istlm  17867  prdsdsf  17931  prdsxmet  17933  xpsxmetlem  17943  xpsmet  17946  isms  17995  mspropd  18020  setsxms  18025  setsms  18026  tmsxms  18032  tmsms  18033  imasf1oxms  18035  imasf1oms  18036  prdsmslem1  18073  prdsxmslem1  18074  tmsxpsval  18084  tngngp2  18168  isnrg  18171  tngnrg  18185  bcthlem2  18747  bcthlem3  18748  bcthlem4  18749  bcthlem5  18750  iscms  18767  cmspropd  18771  cmsss  18772  minveclem3a  18791  shft2rab  18867  ovolicc2lem3  18878  ovolicc2lem4  18879  ovolicc2lem5  18880  vitalilem2  18964  vitalilem3  18965  vitali  18968  limcfval  19222  limcmpt2  19234  limcres  19236  cnplimc  19237  cnlimci  19239  dvcnp2  19269  elcpn  19283  dvcnvlem  19323  uc1pval  19525  ig1pcl  19561  jensen  20283  imsmet  21260  smcn  21271  iscbn  21443  isibfm  23593  probmeasb  23633  ptpcon  23764  cvmscbv  23789  cvmshmeo  23802  cvmsss2  23805  cvmliftlem7  23822  cvmliftlem10  23825  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  ghomgrplem  23996  elfzp1b  24012  bclelnu  25155  repcpwti  25161  osneisi  25531  istopx  25547  istopxc  25548  prismorcset2  25918  prismorcset3  25938  isray2  26153  isray  26154  upixp  26403  sdclem1  26453  sstotbnd2  26498  prdsbnd  26517  prdstotbnd  26518  prdsbnd2  26519  cnpwstotbnd  26521  repwsmet  26558  isprrngo  26675  isnacs3  26785  nacsfix  26787  mzpclall  26805  dnnumch1  27141  dnwech  27145  aomclem3  27153  aomclem8  27159  dfac11  27160  islmodfg  27167  frlmlbs  27249  islindf  27282  islinds2  27283  lindfind  27286  lindsind  27287  lindsind2  27289  lindfrn  27291  lindfmm  27297  lsslindf  27300  sblpnf  27539  rusbcALT  27639  climsuselem1  27733  climsuse  27734  stoweidlem26  27775  stoweidlem31  27780  stoweidlem59  27808  dfateq12d  27992  nbgraop  28140  isopos  29370  isatl  29489
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-cleq 2276  df-clel 2279
  Copyright terms: Public domain W3C validator