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

Theorem eleq12d 2506
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 2505 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2504 . 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 1369    e. wcel 1756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431  df-clel 2434
This theorem is referenced by:  cbvraldva2  2946  cbvrexdva2  2947  cdeqel  3177  ru  3180  sbceqbid  3188  cbvralcsf  3314  cbvreucsf  3316  cbvrabcsf  3317  sbcel12  3670  sbcel12gOLD  3671  elvvuni  4894  elrnmpt1  5083  canth  6044  onnseq  6797  smoeq  6803  smores  6805  smores2  6807  iordsmo  6810  tz7.49  6892  nnaordr  7051  omsmolem  7084  fvixp  7260  cbvixp  7272  mptelixpg  7292  boxcutc  7298  ixpiunwdom  7798  elirr  7805  cantnflt  7872  oemapvali  7884  cantnflem1  7889  cantnf  7893  cantnfltOLD  7902  cantnflem1OLD  7912  cantnfOLD  7915  wemapwe  7920  wemapweOLD  7921  cnfcom3lem  7928  cnfcom3lemOLD  7936  infxpen  8173  dfac8alem  8191  dfac8clem  8194  ac5num  8198  acni2  8208  numacn  8211  acndom  8213  aceq3lem  8282  dfac5  8290  dfac9  8297  dfac13  8303  fin2i  8456  isfin2-2  8480  fin23lem27  8489  isfin3ds  8490  fin23lem17  8499  fin23lem39  8511  isf33lem  8527  isf34lem7  8540  isf34lem6  8541  fin1a2lem10  8570  fin1a2lem12  8572  hsmexlem4  8590  axcc2lem  8597  axcc3  8599  domtriomlem  8603  axdc2lem  8609  axdc3lem2  8612  axdc3lem3  8613  axdc3lem4  8614  axdc3  8615  axdc4lem  8616  axcclem  8618  ac6num  8640  ac6c4  8642  iundom2g  8696  fpwwe2  8802  pwfseqlem1  8817  pwfseqlem4a  8820  pwfseqlem4  8821  ltapi  9064  ltmpi  9065  eluzadd  10881  fzsubel  11486  elfzp1b  11529  axdc4uzlem  11796  wrd2ind  12364  smuval  13669  prdsbasprj  14402  xpsfrnel  14493  ismri2dad  14567  mreexd  14572  mreacs  14588  iscat  14602  iscatd  14603  iscatd2  14611  catcocl  14615  catpropd  14640  brssc  14719  issubc  14740  subcidcl  14746  subccocl  14747  isfunc  14766  isfuncd  14767  cofucl  14790  funcres2b  14799  fuciso  14877  yonedalem3  15082  yonffthlem  15084  ismnd  15409  ismndd  15436  eqgfval  15720  efgsdm  16218  efgsdmi  16220  efgsrel  16222  efgsp1  16225  efgsres  16226  dprdwd  16483  dprdfcl  16485  dprdwdOLD  16489  dprdfclOLD  16491  ablfaclem3  16576  isdrngd  16835  issrng  16913  issrngd  16924  islmodd  16932  islbs  17134  lbsind  17138  lbspropd  17157  islbs2  17212  lbsextlem4  17219  lbsextg  17220  zndvds  17957  isphl  18032  isphld  18058  phlpropd  18059  frlmlbs  18200  islindf  18216  islinds2  18217  lindfind  18220  lindsind  18221  lindsind2  18223  lindfrn  18225  lindfmm  18231  lsslindf  18234  istps  18516  tpspropd  18520  eltpsg  18525  islp  18719  1stcelcls  19040  kgeni  19085  kgencn2  19105  ptpjpre1  19119  elptr2  19122  ptbasin  19125  ptbasfi  19129  ptpjcn  19159  ptpjopn  19160  ptcld  19161  ptcldmpt  19162  ptclsg  19163  ptcnp  19170  qtopval  19243  ptcmplem2  19600  ptcmplem3  19601  ptcmplem4  19602  istmd  19620  istgp  19623  tmdgsum  19641  istlm  19734  isusp  19811  prdsdsf  19917  prdsxmet  19919  isms  19999  mspropd  20024  setsxms  20029  setsms  20030  tmsxms  20036  tmsms  20037  isnrg  20216  tngnrg  20230  bcthlem2  20811  bcthlem3  20812  bcthlem4  20813  bcthlem5  20814  iscms  20831  cmspropd  20835  cmsss  20836  shft2rab  20966  ovolicc2lem3  20977  ovolicc2lem4  20978  ovolicc2lem5  20979  vitalilem2  21064  vitalilem3  21065  vitali  21068  limcfval  21322  limcmpt2  21334  limcres  21336  cnplimc  21337  cnlimci  21339  elcpn  21383  uc1pval  21586  ig1pcl  21622  jensen  22357  axtgcont  22905  tglngval  22959  mirbtwnb  23041  f1otrg  23068  nbgraop  23286  imsmet  24033  smcn  24044  iscbn  24216  sbceqbidf  25816  isslmd  26169  zhmnrg  26348  eulerpartlemgvv  26711  eulerpart  26717  ptpcon  27074  cvmscbv  27099  cvmshmeo  27112  cvmsss2  27115  cvmliftlem7  27132  cvmliftlem10  27135  cvmlift2lem11  27154  cvmlift2lem12  27155  ghomgrplem  27259  ptrest  28378  mbfposadd  28392  upixp  28576  sdclem1  28592  sstotbnd2  28626  prdsbnd2  28647  isprrngo  28803  isnacs3  28999  nacsfix  29001  mzpclall  29016  dnnumch1  29350  dnwech  29354  aomclem3  29362  aomclem8  29367  dfac11  29368  islmodfg  29375  sblpnf  29549  rusbcALT  29646  climsuselem1  29733  climsuse  29734  stoweidlem31  29779  stoweidlem59  29807  dfateq12d  29988  mat1dimmul  30795  islininds  30869  isopos  32665  isatl  32784
  Copyright terms: Public domain W3C validator