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

Theorem eleq12d 2503
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 2502 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2501 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 245 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725
This theorem is referenced by:  cbvraldva2  2928  cbvrexdva2  2929  cdeqel  3149  ru  3152  sbcel12g  3258  cbvralcsf  3303  cbvreucsf  3305  cbvrabcsf  3306  elvvuni  4930  elrnmpt1  5111  canth  6531  onnseq  6598  smoeq  6604  smores  6606  smores2  6608  iordsmo  6611  tz7.49  6694  nnaordr  6855  omsmolem  6888  fvixp  7059  cbvixp  7071  mptelixpg  7091  boxcutc  7097  ixpiunwdom  7551  elirr  7558  cantnflt  7619  oemapvali  7632  cantnflem1  7637  cantnf  7641  wemapwe  7646  cnfcom3lem  7652  infxpen  7888  dfac8alem  7902  dfac8clem  7905  ac5num  7909  acni2  7919  numacn  7922  acndom  7924  aceq3lem  7993  dfac5  8001  dfac9  8008  dfac13  8014  fin2i  8167  isfin2-2  8191  fin23lem27  8200  isfin3ds  8201  fin23lem17  8210  fin23lem39  8222  isf33lem  8238  isf34lem7  8251  isf34lem6  8252  fin1a2lem10  8281  fin1a2lem12  8283  hsmexlem4  8301  axcc2lem  8308  axcc3  8310  domtriomlem  8314  axdc2lem  8320  axdc3lem2  8323  axdc3lem3  8324  axdc3lem4  8325  axdc3  8326  axdc4lem  8327  axcclem  8329  ac6num  8351  ac6c4  8353  iundom2g  8407  fpwwe2  8510  pwfseqlem1  8525  pwfseqlem4a  8528  pwfseqlem4  8529  ltapi  8772  ltmpi  8773  eluzadd  10506  fzsubel  11080  axdc4uzlem  11313  smuval  12985  prdsbasprj  13686  xpsfrnel  13780  ismri2dad  13854  mreexd  13859  mreacs  13875  iscat  13889  iscatd  13890  iscatd2  13898  catcocl  13902  catpropd  13927  brssc  14006  issubc  14027  subcidcl  14033  subccocl  14034  isfunc  14053  isfuncd  14054  cofucl  14077  funcres2b  14086  fuciso  14164  yonedalem3  14369  yonffthlem  14371  islat  14468  isclat  14530  isla  14657  ismnd  14684  ismndd  14711  eqgfval  14980  efgsdm  15354  efgsdmi  15356  efgsrel  15358  efgsp1  15361  efgsres  15362  dprdwd  15561  dprdfcl  15563  ablfaclem3  15637  isdrngd  15852  issrng  15930  issrngd  15941  islmodd  15948  islbs  16140  lbsind  16144  lbspropd  16163  islbs2  16218  lbsextlem4  16225  lbsextg  16226  zndvds  16822  isphl  16851  isphld  16877  phlpropd  16878  istps  16993  tpspropd  16997  eltpsg  17002  islp  17196  1stcelcls  17516  kgeni  17561  kgencn2  17581  ptpjpre1  17595  elptr2  17598  ptbasin  17601  ptbasfi  17605  ptpjcn  17635  ptpjopn  17636  ptcld  17637  ptcldmpt  17638  ptclsg  17639  ptcnp  17646  qtopval  17719  ptcmplem2  18076  ptcmplem3  18077  ptcmplem4  18078  istmd  18096  istgp  18099  tmdgsum  18117  istlm  18206  isusp  18283  prdsdsf  18389  prdsxmet  18391  isms  18471  mspropd  18496  setsxms  18501  setsms  18502  tmsxms  18508  tmsms  18509  isnrg  18688  tngnrg  18702  bcthlem2  19270  bcthlem3  19271  bcthlem4  19272  bcthlem5  19273  iscms  19290  cmspropd  19294  cmsss  19295  shft2rab  19396  ovolicc2lem3  19407  ovolicc2lem4  19408  ovolicc2lem5  19409  vitalilem2  19493  vitalilem3  19494  vitali  19497  limcfval  19751  limcmpt2  19763  limcres  19765  cnplimc  19766  cnlimci  19768  elcpn  19812  uc1pval  20054  ig1pcl  20090  jensen  20819  nbgraop  21428  imsmet  22175  smcn  22186  iscbn  22358  zhmnrg  24343  ptpcon  24912  cvmscbv  24937  cvmshmeo  24950  cvmsss2  24953  cvmliftlem7  24970  cvmliftlem10  24973  cvmlift2lem11  24992  cvmlift2lem12  24993  ghomgrplem  25092  elfzp1b  25108  upixp  26422  sdclem1  26438  sstotbnd2  26474  prdsbnd2  26495  isprrngo  26651  isnacs3  26755  nacsfix  26757  mzpclall  26775  dnnumch1  27110  dnwech  27114  aomclem3  27122  aomclem8  27127  dfac11  27128  islmodfg  27135  frlmlbs  27217  islindf  27250  islinds2  27251  lindfind  27254  lindsind  27255  lindsind2  27257  lindfrn  27259  lindfmm  27265  lsslindf  27268  sblpnf  27507  rusbcALT  27607  climsuselem1  27700  climsuse  27701  stoweidlem31  27747  stoweidlem59  27775  dfateq12d  27960  isopos  29915  isatl  30034
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-clel 2431
  Copyright terms: Public domain W3C validator