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

Theorem eleq12d 2464
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq2d.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 2452 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq2d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2451 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 253 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1399    e. wcel 1826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1621  df-cleq 2374  df-clel 2377
This theorem is referenced by:  neleq12d  2719  cbvraldva2  3013  cbvrexdva2  3014  cdeqel  3248  ru  3251  sbceqbid  3259  cbvralcsf  3380  cbvreucsf  3382  cbvrabcsf  3383  sbcel12  3750  elvvuni  4974  elrnmpt1  5164  canth  6155  onnseq  6933  smoeq  6939  smores  6941  smores2  6943  iordsmo  6946  tz7.49  7028  nnaordr  7187  omsmolem  7220  fvixp  7393  cbvixp  7405  mptelixpg  7425  boxcutc  7431  ixpiunwdom  7932  elirr  7939  cantnflt  8004  oemapvali  8016  cantnflem1  8021  cantnf  8025  cantnfltOLD  8034  cantnflem1OLD  8044  cantnfOLD  8047  wemapwe  8052  wemapweOLD  8053  cnfcom3lem  8060  cnfcom3lemOLD  8068  infxpen  8305  dfac8alem  8323  dfac8clem  8326  ac5num  8330  acni2  8340  numacn  8343  acndom  8345  aceq3lem  8414  dfac5  8422  dfac9  8429  dfac13  8435  fin2i  8588  isfin2-2  8612  fin23lem27  8621  isfin3ds  8622  fin23lem17  8631  fin23lem39  8643  isf33lem  8659  isf34lem7  8672  isf34lem6  8673  fin1a2lem10  8702  fin1a2lem12  8704  hsmexlem4  8722  axcc2lem  8729  axcc3  8731  domtriomlem  8735  axdc2lem  8741  axdc3lem2  8744  axdc3lem3  8745  axdc3lem4  8746  axdc3  8747  axdc4lem  8748  axcclem  8750  ac6num  8772  ac6c4  8774  iundom2g  8828  fpwwe2  8932  pwfseqlem1  8947  pwfseqlem4a  8950  pwfseqlem4  8951  ltapi  9192  ltmpi  9193  eluzadd  11029  fzsubel  11641  elfzp1b  11677  axdc4uzlem  11995  wrd2ind  12614  smuval  14133  prdsbasprj  14879  xpsfrnel  14970  ismri2dad  15044  mreexd  15049  mreacs  15065  iscat  15079  iscatd  15080  iscatd2  15088  catcocl  15092  catpropd  15115  brssc  15220  issubc  15241  subcidcl  15250  subccocl  15251  isfunc  15270  isfuncd  15271  cofucl  15294  funcres2b  15303  fuciso  15381  yonedalem3  15666  yonffthlem  15668  ismgm  15990  ismndOLD  16043  ismndd  16060  eqgfval  16366  efgsdm  16865  efgsdmi  16867  efgsrel  16869  efgsp1  16872  efgsres  16873  dprdwdOLD2  17158  dprdfcl  17160  dprdwdOLD  17164  dprdfclOLD  17166  ablfaclem3  17251  isdrngd  17534  issrng  17612  issrngd  17623  islmodd  17631  islbs  17835  lbsind  17839  lbspropd  17858  islbs2  17913  lbsextlem4  17920  lbsextg  17921  zndvds  18679  isphl  18754  isphld  18780  phlpropd  18781  frlmlbs  18917  islindf  18932  islinds2  18933  lindfind  18936  lindsind  18937  lindsind2  18939  lindfrn  18941  lindfmm  18947  lsslindf  18950  mat1dimmul  19063  istps  19522  tpspropd  19526  eltpsg  19531  islp  19727  1stcelcls  20047  kgeni  20123  kgencn2  20143  ptpjpre1  20157  elptr2  20160  ptbasin  20163  ptbasfi  20167  ptpjcn  20197  ptpjopn  20198  ptcld  20199  ptcldmpt  20200  ptclsg  20201  ptcnp  20208  qtopval  20281  ptcmplem2  20638  ptcmplem3  20639  ptcmplem4  20640  istmd  20658  istgp  20661  tmdgsum  20679  istlm  20772  isusp  20849  prdsdsf  20955  prdsxmet  20957  isms  21037  mspropd  21062  setsxms  21067  setsms  21068  tmsxms  21074  tmsms  21075  isnrg  21254  tngnrg  21268  bcthlem2  21849  bcthlem3  21850  bcthlem4  21851  bcthlem5  21852  iscms  21869  cmspropd  21873  cmsss  21874  shft2rab  22004  ovolicc2lem3  22015  ovolicc2lem4  22016  ovolicc2lem5  22017  vitalilem2  22103  vitalilem3  22104  vitali  22107  limcfval  22361  limcmpt2  22373  limcres  22375  cnplimc  22376  cnlimci  22378  elcpn  22422  uc1pval  22625  ig1pcl  22661  jensen  23435  axtgcont  23983  tglngval  24058  ishlg  24106  mirbtwnb  24172  iscgra  24289  cgraid  24290  nbgraop  24544  nbgraopALT  24545  imsmet  25714  smcn  25725  iscbn  25897  sbceqbidf  27497  isslmd  27898  ispcmp  28014  zhmnrg  28101  ismntoplly  28156  sigapildsys  28307  fiunelcarsg  28443  eulerpartlemgvv  28498  eulerpart  28504  ptpcon  28867  cvmscbv  28892  cvmshmeo  28905  cvmsss2  28908  cvmliftlem7  28925  cvmliftlem10  28928  cvmlift2lem11  28947  cvmlift2lem12  28948  elmpps  29122  ghomgrplem  29218  ptrest  30213  upixp  30386  sdclem1  30402  sstotbnd2  30436  prdsbnd2  30457  isprrngo  30613  isnacs3  30808  nacsfix  30810  mzpclall  30825  dnnumch1  31156  dnwech  31160  aomclem3  31168  aomclem8  31173  dfac11  31174  islmodfg  31181  sblpnf  31358  rusbcALT  31514  climsuselem1  31779  climsuse  31780  cncfuni  31855  dvnprodlem1  31909  stoweidlem31  31979  stoweidlem59  32007  fourierdlem46  32101  fourierdlem62  32117  fourierdlem72  32127  fourierdlem79  32134  fourierdlem88  32143  fourierdlem89  32144  fourierdlem90  32145  fourierdlem91  32146  fourierdlem112  32167  dfateq12d  32380  ismgmd  32782  iscllaw  32831  islininds  33247  sbcel12gOLD  33651  isopos  35318  isatl  35437
  Copyright terms: Public domain W3C validator