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

Theorem eleq12d 2501
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq12d.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 2492 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq12d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2491 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 256 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    e. wcel 1872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-cleq 2414  df-clel 2417
This theorem is referenced by:  neleq12d  2758  cbvraldva2  3058  cbvrexdva2  3059  cdeqel  3295  ru  3298  sbceqbid  3306  cbvralcsf  3427  cbvreucsf  3429  cbvrabcsf  3430  sbcel12  3802  elvvuni  4914  elrnmpt1  5102  canth  6264  onnseq  7074  smoeq  7080  smores  7082  smores2  7084  iordsmo  7087  tz7.49  7173  nnaordr  7332  omsmolem  7365  fvixp  7538  cbvixp  7550  mptelixpg  7570  boxcutc  7576  ixpiunwdom  8115  elirr  8122  cantnflt  8185  oemapvali  8197  cantnflem1  8202  cantnf  8206  wemapwe  8210  cnfcom3lem  8216  infxpen  8453  dfac8alem  8467  dfac8clem  8470  ac5num  8474  acni2  8484  numacn  8487  acndom  8489  aceq3lem  8558  dfac5  8566  dfac9  8573  dfac13  8579  fin2i  8732  isfin2-2  8756  fin23lem27  8765  isfin3ds  8766  fin23lem17  8775  fin23lem39  8787  isf33lem  8803  isf34lem7  8816  isf34lem6  8817  fin1a2lem10  8846  fin1a2lem12  8848  hsmexlem4  8866  axcc2lem  8873  axcc3  8875  domtriomlem  8879  axdc2lem  8885  axdc3lem2  8888  axdc3lem3  8889  axdc3lem4  8890  axdc3  8891  axdc4lem  8892  axcclem  8894  ac6num  8916  ac6c4  8918  iundom2g  8972  fpwwe2  9075  pwfseqlem1  9090  pwfseqlem4a  9093  pwfseqlem4  9094  ltapi  9335  ltmpi  9336  eluzadd  11194  fzsubel  11841  elfzp1b  11878  axdc4uzlem  12201  wrd2ind  12836  smuval  14454  prdsbasprj  15369  xpsfrnel  15468  ismri2dad  15542  mreexd  15547  mreacs  15563  iscat  15577  iscatd  15578  iscatd2  15586  catcocl  15590  catpropd  15613  brssc  15718  issubc  15739  subcidcl  15748  subccocl  15749  isfunc  15768  isfuncd  15769  cofucl  15792  funcres2b  15801  fuciso  15879  yonedalem3  16164  yonffthlem  16166  ismgm  16488  ismndOLD  16541  ismndd  16558  eqgfval  16864  efgsdm  17379  efgsdmi  17381  efgsrel  17383  efgsp1  17386  efgsres  17387  dprdwdOLD  17643  dprdfcl  17645  ablfaclem3  17719  isdrngd  17999  issrng  18077  issrngd  18088  islmodd  18096  islbs  18298  lbsind  18302  lbspropd  18321  islbs2  18376  lbsextlem4  18383  lbsextg  18384  zndvds  19118  isphl  19193  isphld  19219  phlpropd  19220  frlmlbs  19353  islindf  19368  islinds2  19369  lindfind  19372  lindsind  19373  lindsind2  19375  lindfrn  19377  lindfmm  19383  lsslindf  19386  mat1dimmul  19499  istps  19949  tpspropd  19953  eltpsg  19958  islp  20154  1stcelcls  20474  kgeni  20550  kgencn2  20570  ptpjpre1  20584  elptr2  20587  ptbasin  20590  ptbasfi  20594  ptpjcn  20624  ptpjopn  20625  ptcld  20626  ptcldmpt  20627  ptclsg  20628  ptcnp  20635  qtopval  20708  ptcmplem2  21066  ptcmplem3  21067  ptcmplem4  21068  istmd  21087  istgp  21090  tmdgsum  21108  istlm  21197  isusp  21274  prdsdsf  21380  prdsxmet  21382  isms  21462  mspropd  21487  setsxms  21492  setsms  21493  tmsxms  21499  tmsms  21500  isnrg  21661  tngnrg  21675  bcthlem2  22291  bcthlem3  22292  bcthlem4  22293  bcthlem5  22294  iscms  22311  cmspropd  22315  cmsss  22316  shft2rab  22459  ovolicc2lem3  22470  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  vitalilem2  22565  vitalilem3  22566  vitali  22569  limcfval  22825  limcmpt2  22837  limcres  22839  cnplimc  22840  cnlimci  22842  elcpn  22886  uc1pval  23088  ig1pcl  23125  ig1pclOLD  23131  jensen  23912  axtgcont  24515  tglngval  24594  ishlg  24645  mirbtwnb  24715  islnopp  24779  outpasch  24795  colhp  24810  trgcopy  24844  trgcopyeu  24846  dfcgra2  24869  acopyeu  24873  isinag  24877  tgasa1  24887  nbgraop  25149  nbgraopALT  25150  imsmet  26321  smcn  26332  iscbn  26504  sbceqbidf  28115  isslmd  28525  submateq  28643  lmatcl  28650  ispcmp  28692  zhmnrg  28779  ismntoplly  28837  inelpisys  28984  sigapildsys  28992  fiunelcarsg  29156  eulerpartlemgvv  29217  eulerpart  29223  ptpcon  29964  cvmscbv  29989  cvmshmeo  30002  cvmsss2  30005  cvmliftlem7  30022  cvmliftlem10  30025  cvmlift2lem11  30044  cvmlift2lem12  30045  elmpps  30219  ghomgrplem  30315  csbfinxpg  31744  ptrest  31903  upixp  32020  sdclem1  32036  sstotbnd2  32070  prdsbnd2  32091  isprrngo  32247  isopos  32715  isatl  32834  isnacs3  35521  nacsfix  35523  mzpclall  35538  dnnumch1  35872  dnwech  35876  aomclem3  35884  aomclem8  35889  dfac11  35890  islmodfg  35897  sblpnf  36628  rusbcALT  36760  sbcel12gOLD  36875  climsuselem1  37626  climsuse  37627  cncfuni  37704  dvnprodlem1  37761  stoweidlem31  37832  stoweidlem59  37860  fourierdlem46  37956  fourierdlem62  37972  fourierdlem72  37982  fourierdlem79  37989  fourierdlem88  37998  fourierdlem89  37999  fourierdlem90  38000  fourierdlem91  38001  fourierdlem112  38022  issal  38096  sge0tsms  38130  sge0iunmpt  38168  ovnsubaddlem1  38296  ovnsubaddlem2  38297  hoidmvlelem3  38323  hoidmvlelem4  38324  dfateq12d  38501  ismgmd  39395  iscllaw  39444  islininds  39860
  Copyright terms: Public domain W3C validator