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
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 2500 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2499 . 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 1362    e. wcel 1755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-cleq 2426  df-clel 2429
This theorem is referenced by:  cbvraldva2  2941  cbvrexdva2  2942  cdeqel  3171  ru  3174  cbvralcsf  3307  cbvreucsf  3309  cbvrabcsf  3310  sbcel12  3663  sbcel12gOLD  3664  elvvuni  4886  elrnmpt1  5075  canth  6036  onnseq  6791  smoeq  6797  smores  6799  smores2  6801  iordsmo  6804  tz7.49  6886  nnaordr  7047  omsmolem  7080  fvixp  7256  cbvixp  7268  mptelixpg  7288  boxcutc  7294  ixpiunwdom  7794  elirr  7801  cantnflt  7868  oemapvali  7880  cantnflem1  7885  cantnf  7889  cantnfltOLD  7898  cantnflem1OLD  7908  cantnfOLD  7911  wemapwe  7916  wemapweOLD  7917  cnfcom3lem  7924  cnfcom3lemOLD  7932  infxpen  8169  dfac8alem  8187  dfac8clem  8190  ac5num  8194  acni2  8204  numacn  8207  acndom  8209  aceq3lem  8278  dfac5  8286  dfac9  8293  dfac13  8299  fin2i  8452  isfin2-2  8476  fin23lem27  8485  isfin3ds  8486  fin23lem17  8495  fin23lem39  8507  isf33lem  8523  isf34lem7  8536  isf34lem6  8537  fin1a2lem10  8566  fin1a2lem12  8568  hsmexlem4  8586  axcc2lem  8593  axcc3  8595  domtriomlem  8599  axdc2lem  8605  axdc3lem2  8608  axdc3lem3  8609  axdc3lem4  8610  axdc3  8611  axdc4lem  8612  axcclem  8614  ac6num  8636  ac6c4  8638  iundom2g  8692  fpwwe2  8797  pwfseqlem1  8812  pwfseqlem4a  8815  pwfseqlem4  8816  ltapi  9059  ltmpi  9060  eluzadd  10876  fzsubel  11480  elfzp1b  11520  axdc4uzlem  11787  wrd2ind  12355  smuval  13659  prdsbasprj  14392  xpsfrnel  14483  ismri2dad  14557  mreexd  14562  mreacs  14578  iscat  14592  iscatd  14593  iscatd2  14601  catcocl  14605  catpropd  14630  brssc  14709  issubc  14730  subcidcl  14736  subccocl  14737  isfunc  14756  isfuncd  14757  cofucl  14780  funcres2b  14789  fuciso  14867  yonedalem3  15072  yonffthlem  15074  ismnd  15399  ismndd  15426  eqgfval  15708  efgsdm  16206  efgsdmi  16208  efgsrel  16210  efgsp1  16213  efgsres  16214  dprdwd  16468  dprdfcl  16470  dprdwdOLD  16474  dprdfclOLD  16476  ablfaclem3  16561  isdrngd  16780  issrng  16858  issrngd  16869  islmodd  16877  islbs  17078  lbsind  17082  lbspropd  17101  islbs2  17156  lbsextlem4  17163  lbsextg  17164  zndvds  17823  isphl  17898  isphld  17924  phlpropd  17925  frlmlbs  18066  islindf  18082  islinds2  18083  lindfind  18086  lindsind  18087  lindsind2  18089  lindfrn  18091  lindfmm  18097  lsslindf  18100  istps  18382  tpspropd  18386  eltpsg  18391  islp  18585  1stcelcls  18906  kgeni  18951  kgencn2  18971  ptpjpre1  18985  elptr2  18988  ptbasin  18991  ptbasfi  18995  ptpjcn  19025  ptpjopn  19026  ptcld  19027  ptcldmpt  19028  ptclsg  19029  ptcnp  19036  qtopval  19109  ptcmplem2  19466  ptcmplem3  19467  ptcmplem4  19468  istmd  19486  istgp  19489  tmdgsum  19507  istlm  19600  isusp  19677  prdsdsf  19783  prdsxmet  19785  isms  19865  mspropd  19890  setsxms  19895  setsms  19896  tmsxms  19902  tmsms  19903  isnrg  20082  tngnrg  20096  bcthlem2  20677  bcthlem3  20678  bcthlem4  20679  bcthlem5  20680  iscms  20697  cmspropd  20701  cmsss  20702  shft2rab  20832  ovolicc2lem3  20843  ovolicc2lem4  20844  ovolicc2lem5  20845  vitalilem2  20930  vitalilem3  20931  vitali  20934  limcfval  21188  limcmpt2  21200  limcres  21202  cnplimc  21203  cnlimci  21205  elcpn  21249  uc1pval  21495  ig1pcl  21531  jensen  22266  axtgcont  22814  tglngval  22863  mirbtwnb  22936  f1otrg  22939  nbgraop  23157  imsmet  23904  smcn  23915  iscbn  24087  sbceqbid  25687  sbceqbidf  25688  isslmd  26066  zhmnrg  26249  eulerpartlemgvv  26606  eulerpart  26612  ptpcon  26969  cvmscbv  26994  cvmshmeo  27007  cvmsss2  27010  cvmliftlem7  27027  cvmliftlem10  27030  cvmlift2lem11  27049  cvmlift2lem12  27050  ghomgrplem  27154  ptrest  28266  mbfposadd  28280  upixp  28464  sdclem1  28480  sstotbnd2  28514  prdsbnd2  28535  isprrngo  28691  isnacs3  28888  nacsfix  28890  mzpclall  28905  dnnumch1  29239  dnwech  29243  aomclem3  29251  aomclem8  29256  dfac11  29257  islmodfg  29264  sblpnf  29438  rusbcALT  29535  climsuselem1  29623  climsuse  29624  stoweidlem31  29669  stoweidlem59  29697  dfateq12d  29878  islininds  30686  isopos  32395  isatl  32514
  Copyright terms: Public domain W3C validator