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

Theorem eleq12d 2525
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 2513 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq2d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2512 . 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 1383    e. wcel 1804
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-cleq 2435  df-clel 2438
This theorem is referenced by:  neleq12d  2780  cbvraldva2  3074  cbvrexdva2  3075  cdeqel  3309  ru  3312  sbceqbid  3320  cbvralcsf  3452  cbvreucsf  3454  cbvrabcsf  3455  sbcel12  3809  sbcel12gOLD  3810  elvvuni  5050  elrnmpt1  5241  canth  6239  onnseq  7017  smoeq  7023  smores  7025  smores2  7027  iordsmo  7030  tz7.49  7112  nnaordr  7271  omsmolem  7304  fvixp  7476  cbvixp  7488  mptelixpg  7508  boxcutc  7514  ixpiunwdom  8020  elirr  8027  cantnflt  8094  oemapvali  8106  cantnflem1  8111  cantnf  8115  cantnfltOLD  8124  cantnflem1OLD  8134  cantnfOLD  8137  wemapwe  8142  wemapweOLD  8143  cnfcom3lem  8150  cnfcom3lemOLD  8158  infxpen  8395  dfac8alem  8413  dfac8clem  8416  ac5num  8420  acni2  8430  numacn  8433  acndom  8435  aceq3lem  8504  dfac5  8512  dfac9  8519  dfac13  8525  fin2i  8678  isfin2-2  8702  fin23lem27  8711  isfin3ds  8712  fin23lem17  8721  fin23lem39  8733  isf33lem  8749  isf34lem7  8762  isf34lem6  8763  fin1a2lem10  8792  fin1a2lem12  8794  hsmexlem4  8812  axcc2lem  8819  axcc3  8821  domtriomlem  8825  axdc2lem  8831  axdc3lem2  8834  axdc3lem3  8835  axdc3lem4  8836  axdc3  8837  axdc4lem  8838  axcclem  8840  ac6num  8862  ac6c4  8864  iundom2g  8918  fpwwe2  9024  pwfseqlem1  9039  pwfseqlem4a  9042  pwfseqlem4  9043  ltapi  9284  ltmpi  9285  eluzadd  11120  fzsubel  11730  elfzp1b  11766  axdc4uzlem  12074  wrd2ind  12685  smuval  14113  prdsbasprj  14851  xpsfrnel  14942  ismri2dad  15016  mreexd  15021  mreacs  15037  iscat  15051  iscatd  15052  iscatd2  15060  catcocl  15064  catpropd  15086  brssc  15165  issubc  15186  subcidcl  15192  subccocl  15193  isfunc  15212  isfuncd  15213  cofucl  15236  funcres2b  15245  fuciso  15323  yonedalem3  15528  yonffthlem  15530  ismgm  15852  ismndOLD  15905  ismndd  15922  eqgfval  16228  efgsdm  16727  efgsdmi  16729  efgsrel  16731  efgsp1  16734  efgsres  16735  dprdwdOLD2  17024  dprdfcl  17026  dprdwdOLD  17030  dprdfclOLD  17032  ablfaclem3  17117  isdrngd  17400  issrng  17478  issrngd  17489  islmodd  17497  islbs  17701  lbsind  17705  lbspropd  17724  islbs2  17779  lbsextlem4  17786  lbsextg  17787  zndvds  18566  isphl  18641  isphld  18667  phlpropd  18668  frlmlbs  18809  islindf  18825  islinds2  18826  lindfind  18829  lindsind  18830  lindsind2  18832  lindfrn  18834  lindfmm  18840  lsslindf  18843  mat1dimmul  18956  istps  19415  tpspropd  19419  eltpsg  19424  islp  19619  1stcelcls  19940  kgeni  20016  kgencn2  20036  ptpjpre1  20050  elptr2  20053  ptbasin  20056  ptbasfi  20060  ptpjcn  20090  ptpjopn  20091  ptcld  20092  ptcldmpt  20093  ptclsg  20094  ptcnp  20101  qtopval  20174  ptcmplem2  20531  ptcmplem3  20532  ptcmplem4  20533  istmd  20551  istgp  20554  tmdgsum  20572  istlm  20665  isusp  20742  prdsdsf  20848  prdsxmet  20850  isms  20930  mspropd  20955  setsxms  20960  setsms  20961  tmsxms  20967  tmsms  20968  isnrg  21147  tngnrg  21161  bcthlem2  21742  bcthlem3  21743  bcthlem4  21744  bcthlem5  21745  iscms  21762  cmspropd  21766  cmsss  21767  shft2rab  21897  ovolicc2lem3  21908  ovolicc2lem4  21909  ovolicc2lem5  21910  vitalilem2  21996  vitalilem3  21997  vitali  22000  limcfval  22254  limcmpt2  22266  limcres  22268  cnplimc  22269  cnlimci  22271  elcpn  22315  uc1pval  22518  ig1pcl  22554  jensen  23296  axtgcont  23844  tglngval  23916  ishlg  23964  mirbtwnb  24030  nbgraop  24401  nbgraopALT  24402  imsmet  25575  smcn  25586  iscbn  25758  sbceqbidf  27358  isslmd  27723  ispcmp  27838  zhmnrg  27926  ismntoplly  27981  eulerpartlemgvv  28293  eulerpart  28299  ptpcon  28656  cvmscbv  28681  cvmshmeo  28694  cvmsss2  28697  cvmliftlem7  28714  cvmliftlem10  28717  cvmlift2lem11  28736  cvmlift2lem12  28737  elmpps  28911  ghomgrplem  29007  ptrest  30024  upixp  30196  sdclem1  30212  sstotbnd2  30246  prdsbnd2  30267  isprrngo  30423  isnacs3  30618  nacsfix  30620  mzpclall  30635  dnnumch1  30966  dnwech  30970  aomclem3  30978  aomclem8  30983  dfac11  30984  islmodfg  30991  sblpnf  31166  rusbcALT  31300  climsuselem1  31567  climsuse  31568  cncfuni  31643  dvnprodlem1  31697  stoweidlem31  31767  stoweidlem59  31795  fourierdlem46  31889  fourierdlem62  31905  fourierdlem72  31915  fourierdlem79  31922  fourierdlem88  31931  fourierdlem89  31932  fourierdlem90  31933  fourierdlem91  31934  fourierdlem112  31955  dfateq12d  32168  ismgmd  32418  iscllaw  32466  islininds  32917  isopos  34780  isatl  34899
  Copyright terms: Public domain W3C validator