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

Theorem eleq12d 2536
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 2524 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq2d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2523 . 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 1370    e. wcel 1758
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-cleq 2446  df-clel 2449
This theorem is referenced by:  neleq12d  2789  cbvraldva2  3057  cbvrexdva2  3058  cdeqel  3290  ru  3293  sbceqbid  3301  cbvralcsf  3430  cbvreucsf  3432  cbvrabcsf  3433  sbcel12  3786  sbcel12gOLD  3787  elvvuni  5010  elrnmpt1  5199  canth  6161  onnseq  6918  smoeq  6924  smores  6926  smores2  6928  iordsmo  6931  tz7.49  7013  nnaordr  7172  omsmolem  7205  fvixp  7381  cbvixp  7393  mptelixpg  7413  boxcutc  7419  ixpiunwdom  7920  elirr  7927  cantnflt  7994  oemapvali  8006  cantnflem1  8011  cantnf  8015  cantnfltOLD  8024  cantnflem1OLD  8034  cantnfOLD  8037  wemapwe  8042  wemapweOLD  8043  cnfcom3lem  8050  cnfcom3lemOLD  8058  infxpen  8295  dfac8alem  8313  dfac8clem  8316  ac5num  8320  acni2  8330  numacn  8333  acndom  8335  aceq3lem  8404  dfac5  8412  dfac9  8419  dfac13  8425  fin2i  8578  isfin2-2  8602  fin23lem27  8611  isfin3ds  8612  fin23lem17  8621  fin23lem39  8633  isf33lem  8649  isf34lem7  8662  isf34lem6  8663  fin1a2lem10  8692  fin1a2lem12  8694  hsmexlem4  8712  axcc2lem  8719  axcc3  8721  domtriomlem  8725  axdc2lem  8731  axdc3lem2  8734  axdc3lem3  8735  axdc3lem4  8736  axdc3  8737  axdc4lem  8738  axcclem  8740  ac6num  8762  ac6c4  8764  iundom2g  8818  fpwwe2  8924  pwfseqlem1  8939  pwfseqlem4a  8942  pwfseqlem4  8943  ltapi  9186  ltmpi  9187  eluzadd  11003  fzsubel  11614  elfzp1b  11657  axdc4uzlem  11924  wrd2ind  12493  smuval  13798  prdsbasprj  14532  xpsfrnel  14623  ismri2dad  14697  mreexd  14702  mreacs  14718  iscat  14732  iscatd  14733  iscatd2  14741  catcocl  14745  catpropd  14770  brssc  14849  issubc  14870  subcidcl  14876  subccocl  14877  isfunc  14896  isfuncd  14897  cofucl  14920  funcres2b  14929  fuciso  15007  yonedalem3  15212  yonffthlem  15214  ismnd  15539  ismndd  15566  eqgfval  15851  efgsdm  16351  efgsdmi  16353  efgsrel  16355  efgsp1  16358  efgsres  16359  dprdwd  16620  dprdfcl  16622  dprdwdOLD  16626  dprdfclOLD  16628  ablfaclem3  16713  isdrngd  16983  issrng  17061  issrngd  17072  islmodd  17080  islbs  17283  lbsind  17287  lbspropd  17306  islbs2  17361  lbsextlem4  17368  lbsextg  17369  zndvds  18110  isphl  18185  isphld  18211  phlpropd  18212  frlmlbs  18353  islindf  18369  islinds2  18370  lindfind  18373  lindsind  18374  lindsind2  18376  lindfrn  18378  lindfmm  18384  lsslindf  18387  istps  18676  tpspropd  18680  eltpsg  18685  islp  18879  1stcelcls  19200  kgeni  19245  kgencn2  19265  ptpjpre1  19279  elptr2  19282  ptbasin  19285  ptbasfi  19289  ptpjcn  19319  ptpjopn  19320  ptcld  19321  ptcldmpt  19322  ptclsg  19323  ptcnp  19330  qtopval  19403  ptcmplem2  19760  ptcmplem3  19761  ptcmplem4  19762  istmd  19780  istgp  19783  tmdgsum  19801  istlm  19894  isusp  19971  prdsdsf  20077  prdsxmet  20079  isms  20159  mspropd  20184  setsxms  20189  setsms  20190  tmsxms  20196  tmsms  20197  isnrg  20376  tngnrg  20390  bcthlem2  20971  bcthlem3  20972  bcthlem4  20973  bcthlem5  20974  iscms  20991  cmspropd  20995  cmsss  20996  shft2rab  21126  ovolicc2lem3  21137  ovolicc2lem4  21138  ovolicc2lem5  21139  vitalilem2  21225  vitalilem3  21226  vitali  21229  limcfval  21483  limcmpt2  21495  limcres  21497  cnplimc  21498  cnlimci  21500  elcpn  21544  uc1pval  21747  ig1pcl  21783  jensen  22518  axtgcont  23066  tglngval  23124  mirbtwnb  23219  f1otrg  23289  nbgraop  23507  imsmet  24254  smcn  24265  iscbn  24437  sbceqbidf  26037  isslmd  26383  zhmnrg  26561  eulerpartlemgvv  26923  eulerpart  26929  ptpcon  27286  cvmscbv  27311  cvmshmeo  27324  cvmsss2  27327  cvmliftlem7  27344  cvmliftlem10  27347  cvmlift2lem11  27366  cvmlift2lem12  27367  ghomgrplem  27472  ptrest  28593  mbfposadd  28607  upixp  28791  sdclem1  28807  sstotbnd2  28841  prdsbnd2  28862  isprrngo  29018  isnacs3  29214  nacsfix  29216  mzpclall  29231  dnnumch1  29565  dnwech  29569  aomclem3  29577  aomclem8  29582  dfac11  29583  islmodfg  29590  sblpnf  29764  rusbcALT  29861  climsuselem1  29948  climsuse  29949  stoweidlem31  29994  stoweidlem59  30022  dfateq12d  30203  mat1dimmul  31058  islininds  31132  isopos  33183  isatl  33302
  Copyright terms: Public domain W3C validator