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

Theorem eleq12d 2384
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 2383 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2382 . 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 1633    e. wcel 1701
This theorem is referenced by:  cbvraldva2  2802  cbvrexdva2  2803  cdeqel  3021  ru  3024  sbcel12g  3130  cbvralcsf  3177  cbvreucsf  3179  cbvrabcsf  3180  elvvuni  4787  elrnmpt1  4965  ovmpt2dxf  6015  canth  6336  onnseq  6403  smoeq  6409  smores  6411  smores2  6413  iordsmo  6416  tz7.49  6499  nnaordr  6660  omsmolem  6693  fvixp  6864  cbvixp  6876  mptelixpg  6896  boxcutc  6902  ixpiunwdom  7350  elirr  7357  cantnflt  7418  oemapvali  7431  cantnflem1  7436  cantnf  7440  wemapwe  7445  cnfcom3lem  7451  infxpen  7687  dfac8alem  7701  dfac8clem  7704  ac5num  7708  acni2  7718  numacn  7721  acndom  7723  aceq3lem  7792  dfac5  7800  dfac9  7807  dfac13  7813  cofsmo  7940  cfsmolem  7941  fin2i  7966  isfin2-2  7990  fin23lem27  7999  isfin3ds  8000  fin23lem17  8009  fin23lem39  8021  isf33lem  8037  isf34lem7  8050  isf34lem6  8051  fin1a2lem10  8080  fin1a2lem12  8082  hsmexlem4  8100  axcc2lem  8107  axcc3  8109  domtriomlem  8113  axdc2lem  8119  axdc3lem2  8122  axdc3lem3  8123  axdc3lem4  8124  axdc3  8125  axdc4lem  8126  axcclem  8128  ac6num  8151  ac6c4  8153  iundom2g  8207  smobeth  8253  fpwwe2  8310  pwfseqlem1  8325  pwfseqlem4a  8328  pwfseqlem4  8329  ltapi  8572  ltmpi  8573  eluzadd  10303  fzsubel  10874  fzosubel  10955  axdc4uzlem  11091  smuval  12719  prdsbasprj  13420  xpsfrnel  13514  ismri2dad  13588  mreexd  13593  mreacs  13609  iscat  13623  iscatd  13624  iscatd2  13632  catcocl  13636  catpropd  13661  brssc  13740  issubc  13761  subcidcl  13767  subccocl  13768  isfunc  13787  isfuncd  13788  cofucl  13811  funcres2b  13820  fuciso  13898  yonedalem3  14103  yonffthlem  14105  islat  14202  isclat  14264  isla  14391  ismnd  14418  ismndd  14445  mndpropd  14447  mulgnndir  14638  imasgrp  14660  subg0cl  14678  subginvcl  14679  eqgfval  14714  efgsdm  15088  efgsdmi  15090  efgsrel  15092  efgsp1  15095  efgsres  15096  efgcpbllemb  15113  dprdwd  15295  dprdfcl  15297  ablfaclem3  15371  isdrngd  15586  issrng  15664  issrngd  15675  islmodd  15682  lmodprop2d  15736  islbs  15878  lbsind  15882  lbspropd  15901  islbs2  15956  lbsextlem4  15963  lbsextg  15964  psraddcl  16177  qsssubdrg  16487  zndvds  16559  isphl  16588  isphld  16614  phlpropd  16615  istps  16730  tpspropd  16734  eltpsg  16739  islp  16928  1stcelcls  17243  kgeni  17288  kgencn2  17308  ptpjpre1  17322  elptr2  17325  ptbasin  17328  ptbasfi  17332  ptpjcn  17361  ptpjopn  17362  ptcld  17363  ptcldmpt  17364  ptclsg  17365  ptcnp  17372  prdstps  17379  qtopval  17442  xpstopnlem1  17556  ptcmplem2  17799  ptcmplem3  17800  ptcmplem4  17801  istmd  17809  istgp  17812  tmdgsum  17830  tsmssub  17883  istlm  17919  prdsdsf  17983  prdsxmet  17985  xpsxmetlem  17995  xpsmet  17998  isms  18047  mspropd  18072  setsxms  18077  setsms  18078  tmsxms  18084  tmsms  18085  imasf1oxms  18087  imasf1oms  18088  prdsmslem1  18125  prdsxmslem1  18126  tmsxpsval  18136  tngngp2  18220  isnrg  18223  tngnrg  18237  bcthlem2  18800  bcthlem3  18801  bcthlem4  18802  bcthlem5  18803  iscms  18820  cmspropd  18824  cmsss  18825  minveclem3a  18844  shft2rab  18920  ovolicc2lem3  18931  ovolicc2lem4  18932  ovolicc2lem5  18933  vitalilem2  19017  vitalilem3  19018  vitali  19021  limcfval  19275  limcmpt2  19287  limcres  19289  cnplimc  19290  cnlimci  19292  dvcnp2  19322  elcpn  19336  dvcnvlem  19376  uc1pval  19578  ig1pcl  19614  jensen  20336  imsmet  21315  smcn  21326  iscbn  21498  isusp  23458  zhmnrg  23548  probmeasb  23862  ptpcon  24048  cvmscbv  24073  cvmshmeo  24086  cvmsss2  24089  cvmliftlem7  24106  cvmliftlem10  24109  cvmlift2lem9  24126  cvmlift2lem11  24128  cvmlift2lem12  24129  ghomgrplem  24280  elfzp1b  24296  upixp  25552  sdclem1  25602  sstotbnd2  25646  prdsbnd  25665  prdstotbnd  25666  prdsbnd2  25667  cnpwstotbnd  25669  repwsmet  25706  isprrngo  25823  isnacs3  25933  nacsfix  25935  mzpclall  25953  dnnumch1  26289  dnwech  26293  aomclem3  26301  aomclem8  26307  dfac11  26308  islmodfg  26315  frlmlbs  26397  islindf  26430  islinds2  26431  lindfind  26434  lindsind  26435  lindsind2  26437  lindfrn  26439  lindfmm  26445  lsslindf  26448  sblpnf  26687  rusbcALT  26787  climsuselem1  26881  climsuse  26882  stoweidlem26  26923  stoweidlem31  26928  stoweidlem59  26956  dfateq12d  27142  nbgraop  27373  isopos  29188  isatl  29307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-11 1732  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1533  df-cleq 2309  df-clel 2312
  Copyright terms: Public domain W3C validator