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

Theorem eleq12d 2511
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 2499 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq2d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2498 . 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 1870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-cleq 2421  df-clel 2424
This theorem is referenced by:  neleq12d  2769  cbvraldva2  3066  cbvrexdva2  3067  cdeqel  3301  ru  3304  sbceqbid  3312  cbvralcsf  3433  cbvreucsf  3435  cbvrabcsf  3436  sbcel12  3806  elvvuni  4915  elrnmpt1  5103  canth  6264  onnseq  7071  smoeq  7077  smores  7079  smores2  7081  iordsmo  7084  tz7.49  7170  nnaordr  7329  omsmolem  7362  fvixp  7535  cbvixp  7547  mptelixpg  7567  boxcutc  7573  ixpiunwdom  8106  elirr  8113  cantnflt  8176  oemapvali  8188  cantnflem1  8193  cantnf  8197  wemapwe  8201  cnfcom3lem  8207  infxpen  8444  dfac8alem  8458  dfac8clem  8461  ac5num  8465  acni2  8475  numacn  8478  acndom  8480  aceq3lem  8549  dfac5  8557  dfac9  8564  dfac13  8570  fin2i  8723  isfin2-2  8747  fin23lem27  8756  isfin3ds  8757  fin23lem17  8766  fin23lem39  8778  isf33lem  8794  isf34lem7  8807  isf34lem6  8808  fin1a2lem10  8837  fin1a2lem12  8839  hsmexlem4  8857  axcc2lem  8864  axcc3  8866  domtriomlem  8870  axdc2lem  8876  axdc3lem2  8879  axdc3lem3  8880  axdc3lem4  8881  axdc3  8882  axdc4lem  8883  axcclem  8885  ac6num  8907  ac6c4  8909  iundom2g  8963  fpwwe2  9067  pwfseqlem1  9082  pwfseqlem4a  9085  pwfseqlem4  9086  ltapi  9327  ltmpi  9328  eluzadd  11187  fzsubel  11832  elfzp1b  11869  axdc4uzlem  12192  wrd2ind  12819  smuval  14429  prdsbasprj  15329  xpsfrnel  15420  ismri2dad  15494  mreexd  15499  mreacs  15515  iscat  15529  iscatd  15530  iscatd2  15538  catcocl  15542  catpropd  15565  brssc  15670  issubc  15691  subcidcl  15700  subccocl  15701  isfunc  15720  isfuncd  15721  cofucl  15744  funcres2b  15753  fuciso  15831  yonedalem3  16116  yonffthlem  16118  ismgm  16440  ismndOLD  16493  ismndd  16510  eqgfval  16816  efgsdm  17315  efgsdmi  17317  efgsrel  17319  efgsp1  17322  efgsres  17323  dprdwdOLD  17579  dprdfcl  17581  ablfaclem3  17655  isdrngd  17935  issrng  18013  issrngd  18024  islmodd  18032  islbs  18234  lbsind  18238  lbspropd  18257  islbs2  18312  lbsextlem4  18319  lbsextg  18320  zndvds  19051  isphl  19126  isphld  19152  phlpropd  19153  frlmlbs  19286  islindf  19301  islinds2  19302  lindfind  19305  lindsind  19306  lindsind2  19308  lindfrn  19310  lindfmm  19316  lsslindf  19319  mat1dimmul  19432  istps  19882  tpspropd  19886  eltpsg  19891  islp  20087  1stcelcls  20407  kgeni  20483  kgencn2  20503  ptpjpre1  20517  elptr2  20520  ptbasin  20523  ptbasfi  20527  ptpjcn  20557  ptpjopn  20558  ptcld  20559  ptcldmpt  20560  ptclsg  20561  ptcnp  20568  qtopval  20641  ptcmplem2  20999  ptcmplem3  21000  ptcmplem4  21001  istmd  21020  istgp  21023  tmdgsum  21041  istlm  21130  isusp  21207  prdsdsf  21313  prdsxmet  21315  isms  21395  mspropd  21420  setsxms  21425  setsms  21426  tmsxms  21432  tmsms  21433  isnrg  21594  tngnrg  21608  bcthlem2  22186  bcthlem3  22187  bcthlem4  22188  bcthlem5  22189  iscms  22206  cmspropd  22210  cmsss  22211  shft2rab  22339  ovolicc2lem3  22350  ovolicc2lem4  22351  ovolicc2lem5  22352  vitalilem2  22444  vitalilem3  22445  vitali  22448  limcfval  22704  limcmpt2  22716  limcres  22718  cnplimc  22719  cnlimci  22721  elcpn  22765  uc1pval  22965  ig1pcl  23001  jensen  23779  axtgcont  24380  tglngval  24456  ishlg  24507  mirbtwnb  24576  islnopp  24638  outpasch  24654  colhp  24668  trgcopy  24702  trgcopyeu  24704  dfcgra2  24726  acopyeu  24728  isinag  24732  tgasa1  24738  nbgraop  24996  nbgraopALT  24997  imsmet  26168  smcn  26179  iscbn  26351  sbceqbidf  27952  isslmd  28356  submateq  28474  lmatcl  28481  ispcmp  28523  zhmnrg  28610  ismntoplly  28668  inelpisys  28815  sigapildsys  28823  fiunelcarsg  28977  eulerpartlemgvv  29035  eulerpart  29041  ptpcon  29744  cvmscbv  29769  cvmshmeo  29782  cvmsss2  29785  cvmliftlem7  29802  cvmliftlem10  29805  cvmlift2lem11  29824  cvmlift2lem12  29825  elmpps  29999  ghomgrplem  30095  ptrest  31642  upixp  31759  sdclem1  31775  sstotbnd2  31809  prdsbnd2  31830  isprrngo  31986  isopos  32454  isatl  32573  isnacs3  35260  nacsfix  35262  mzpclall  35277  dnnumch1  35607  dnwech  35611  aomclem3  35619  aomclem8  35624  dfac11  35625  islmodfg  35632  sblpnf  36294  rusbcALT  36426  sbcel12gOLD  36541  climsuselem1  37257  climsuse  37258  cncfuni  37335  dvnprodlem1  37389  stoweidlem31  37460  stoweidlem59  37488  fourierdlem46  37583  fourierdlem62  37599  fourierdlem72  37609  fourierdlem79  37616  fourierdlem88  37625  fourierdlem89  37626  fourierdlem90  37627  fourierdlem91  37628  fourierdlem112  37649  issal  37721  sge0tsms  37755  sge0iunmpt  37793  dfateq12d  38020  ismgmd  38533  iscllaw  38582  islininds  38998
  Copyright terms: Public domain W3C validator