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

Theorem eleq12d 2549
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 2537 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq2d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2536 . 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 1379    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-cleq 2459  df-clel 2462
This theorem is referenced by:  neleq12d  2804  cbvraldva2  3092  cbvrexdva2  3093  cdeqel  3327  ru  3330  sbceqbid  3338  cbvralcsf  3467  cbvreucsf  3469  cbvrabcsf  3470  sbcel12  3823  sbcel12gOLD  3824  elvvuni  5059  elrnmpt1  5250  canth  6241  onnseq  7015  smoeq  7021  smores  7023  smores2  7025  iordsmo  7028  tz7.49  7110  nnaordr  7269  omsmolem  7302  fvixp  7474  cbvixp  7486  mptelixpg  7506  boxcutc  7512  ixpiunwdom  8016  elirr  8023  cantnflt  8090  oemapvali  8102  cantnflem1  8107  cantnf  8111  cantnfltOLD  8120  cantnflem1OLD  8130  cantnfOLD  8133  wemapwe  8138  wemapweOLD  8139  cnfcom3lem  8146  cnfcom3lemOLD  8154  infxpen  8391  dfac8alem  8409  dfac8clem  8412  ac5num  8416  acni2  8426  numacn  8429  acndom  8431  aceq3lem  8500  dfac5  8508  dfac9  8515  dfac13  8521  fin2i  8674  isfin2-2  8698  fin23lem27  8707  isfin3ds  8708  fin23lem17  8717  fin23lem39  8729  isf33lem  8745  isf34lem7  8758  isf34lem6  8759  fin1a2lem10  8788  fin1a2lem12  8790  hsmexlem4  8808  axcc2lem  8815  axcc3  8817  domtriomlem  8821  axdc2lem  8827  axdc3lem2  8830  axdc3lem3  8831  axdc3lem4  8832  axdc3  8833  axdc4lem  8834  axcclem  8836  ac6num  8858  ac6c4  8860  iundom2g  8914  fpwwe2  9020  pwfseqlem1  9035  pwfseqlem4a  9038  pwfseqlem4  9039  ltapi  9280  ltmpi  9281  eluzadd  11109  fzsubel  11718  elfzp1b  11754  axdc4uzlem  12059  wrd2ind  12665  smuval  13989  prdsbasprj  14726  xpsfrnel  14817  ismri2dad  14891  mreexd  14896  mreacs  14912  iscat  14926  iscatd  14927  iscatd2  14935  catcocl  14939  catpropd  14964  brssc  15043  issubc  15064  subcidcl  15070  subccocl  15071  isfunc  15090  isfuncd  15091  cofucl  15114  funcres2b  15123  fuciso  15201  yonedalem3  15406  yonffthlem  15408  ismnd  15733  ismndd  15760  eqgfval  16051  efgsdm  16551  efgsdmi  16553  efgsrel  16555  efgsp1  16558  efgsres  16559  dprdwd  16844  dprdfcl  16846  dprdwdOLD  16850  dprdfclOLD  16852  ablfaclem3  16937  isdrngd  17216  issrng  17294  issrngd  17305  islmodd  17313  islbs  17517  lbsind  17521  lbspropd  17540  islbs2  17595  lbsextlem4  17602  lbsextg  17603  zndvds  18371  isphl  18446  isphld  18472  phlpropd  18473  frlmlbs  18614  islindf  18630  islinds2  18631  lindfind  18634  lindsind  18635  lindsind2  18637  lindfrn  18639  lindfmm  18645  lsslindf  18648  mat1dimmul  18761  istps  19220  tpspropd  19224  eltpsg  19229  islp  19423  1stcelcls  19744  kgeni  19789  kgencn2  19809  ptpjpre1  19823  elptr2  19826  ptbasin  19829  ptbasfi  19833  ptpjcn  19863  ptpjopn  19864  ptcld  19865  ptcldmpt  19866  ptclsg  19867  ptcnp  19874  qtopval  19947  ptcmplem2  20304  ptcmplem3  20305  ptcmplem4  20306  istmd  20324  istgp  20327  tmdgsum  20345  istlm  20438  isusp  20515  prdsdsf  20621  prdsxmet  20623  isms  20703  mspropd  20728  setsxms  20733  setsms  20734  tmsxms  20740  tmsms  20741  isnrg  20920  tngnrg  20934  bcthlem2  21515  bcthlem3  21516  bcthlem4  21517  bcthlem5  21518  iscms  21535  cmspropd  21539  cmsss  21540  shft2rab  21670  ovolicc2lem3  21681  ovolicc2lem4  21682  ovolicc2lem5  21683  vitalilem2  21769  vitalilem3  21770  vitali  21773  limcfval  22027  limcmpt2  22039  limcres  22041  cnplimc  22042  cnlimci  22044  elcpn  22088  uc1pval  22291  ig1pcl  22327  jensen  23062  axtgcont  23610  tglngval  23682  mirbtwnb  23781  f1otrg  23866  nbgraop  24115  nbgraopALT  24116  imsmet  25289  smcn  25300  iscbn  25472  sbceqbidf  27072  isslmd  27423  zhmnrg  27600  qtophaus  27653  ismntoplly  27659  eulerpartlemgvv  27971  eulerpart  27977  ptpcon  28334  cvmscbv  28359  cvmshmeo  28372  cvmsss2  28375  cvmliftlem7  28392  cvmliftlem10  28395  cvmlift2lem11  28414  cvmlift2lem12  28415  ghomgrplem  28520  ptrest  29641  mbfposadd  29655  upixp  29839  sdclem1  29855  sstotbnd2  29889  prdsbnd2  29910  isprrngo  30066  isnacs3  30262  nacsfix  30264  mzpclall  30279  dnnumch1  30610  dnwech  30614  aomclem3  30622  aomclem8  30627  dfac11  30628  islmodfg  30635  sblpnf  30809  rusbcALT  30940  iocopn  31140  icoopn  31145  climsuselem1  31165  climsuse  31166  sumnnodd  31188  sublimc  31210  reclimc  31211  divlimc  31214  cncfuni  31241  cncfshiftioo  31247  itgiccshift  31314  itgperiod  31315  stoweidlem31  31347  stoweidlem59  31375  dirkercncflem2  31420  dirkercncflem4  31422  fourierdlem32  31455  fourierdlem33  31456  fourierdlem46  31469  fourierdlem48  31471  fourierdlem62  31485  fourierdlem63  31486  fourierdlem72  31495  fourierdlem74  31497  fourierdlem75  31498  fourierdlem76  31499  fourierdlem79  31502  fourierdlem81  31504  fourierdlem88  31511  fourierdlem89  31512  fourierdlem90  31513  fourierdlem91  31514  fourierdlem92  31515  fourierdlem93  31516  fourierdlem103  31526  fourierdlem104  31527  fourierdlem111  31534  fourierdlem112  31535  fouriersw  31548  fouriercn  31549  dfateq12d  31697  ismgmALT  31939  iscllaw  31957  islininds  32137  isopos  33986  isatl  34105
  Copyright terms: Public domain W3C validator