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

Theorem eleq12d 2472
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 2471 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq1d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2470 . 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 1649    e. wcel 1721
This theorem is referenced by:  cbvraldva2  2896  cbvrexdva2  2897  cdeqel  3117  ru  3120  sbcel12g  3226  cbvralcsf  3271  cbvreucsf  3273  cbvrabcsf  3274  elvvuni  4897  elrnmpt1  5078  canth  6498  onnseq  6565  smoeq  6571  smores  6573  smores2  6575  iordsmo  6578  tz7.49  6661  nnaordr  6822  omsmolem  6855  fvixp  7026  cbvixp  7038  mptelixpg  7058  boxcutc  7064  ixpiunwdom  7515  elirr  7522  cantnflt  7583  oemapvali  7596  cantnflem1  7601  cantnf  7605  wemapwe  7610  cnfcom3lem  7616  infxpen  7852  dfac8alem  7866  dfac8clem  7869  ac5num  7873  acni2  7883  numacn  7886  acndom  7888  aceq3lem  7957  dfac5  7965  dfac9  7972  dfac13  7978  fin2i  8131  isfin2-2  8155  fin23lem27  8164  isfin3ds  8165  fin23lem17  8174  fin23lem39  8186  isf33lem  8202  isf34lem7  8215  isf34lem6  8216  fin1a2lem10  8245  fin1a2lem12  8247  hsmexlem4  8265  axcc2lem  8272  axcc3  8274  domtriomlem  8278  axdc2lem  8284  axdc3lem2  8287  axdc3lem3  8288  axdc3lem4  8289  axdc3  8290  axdc4lem  8291  axcclem  8293  ac6num  8315  ac6c4  8317  iundom2g  8371  fpwwe2  8474  pwfseqlem1  8489  pwfseqlem4a  8492  pwfseqlem4  8493  ltapi  8736  ltmpi  8737  eluzadd  10470  fzsubel  11044  axdc4uzlem  11276  smuval  12948  prdsbasprj  13649  xpsfrnel  13743  ismri2dad  13817  mreexd  13822  mreacs  13838  iscat  13852  iscatd  13853  iscatd2  13861  catcocl  13865  catpropd  13890  brssc  13969  issubc  13990  subcidcl  13996  subccocl  13997  isfunc  14016  isfuncd  14017  cofucl  14040  funcres2b  14049  fuciso  14127  yonedalem3  14332  yonffthlem  14334  islat  14431  isclat  14493  isla  14620  ismnd  14647  ismndd  14674  eqgfval  14943  efgsdm  15317  efgsdmi  15319  efgsrel  15321  efgsp1  15324  efgsres  15325  dprdwd  15524  dprdfcl  15526  ablfaclem3  15600  isdrngd  15815  issrng  15893  issrngd  15904  islmodd  15911  islbs  16103  lbsind  16107  lbspropd  16126  islbs2  16181  lbsextlem4  16188  lbsextg  16189  zndvds  16785  isphl  16814  isphld  16840  phlpropd  16841  istps  16956  tpspropd  16960  eltpsg  16965  islp  17159  1stcelcls  17477  kgeni  17522  kgencn2  17542  ptpjpre1  17556  elptr2  17559  ptbasin  17562  ptbasfi  17566  ptpjcn  17596  ptpjopn  17597  ptcld  17598  ptcldmpt  17599  ptclsg  17600  ptcnp  17607  qtopval  17680  ptcmplem2  18037  ptcmplem3  18038  ptcmplem4  18039  istmd  18057  istgp  18060  tmdgsum  18078  istlm  18167  isusp  18244  prdsdsf  18350  prdsxmet  18352  isms  18432  mspropd  18457  setsxms  18462  setsms  18463  tmsxms  18469  tmsms  18470  isnrg  18649  tngnrg  18663  bcthlem2  19231  bcthlem3  19232  bcthlem4  19233  bcthlem5  19234  iscms  19251  cmspropd  19255  cmsss  19256  shft2rab  19357  ovolicc2lem3  19368  ovolicc2lem4  19369  ovolicc2lem5  19370  vitalilem2  19454  vitalilem3  19455  vitali  19458  limcfval  19712  limcmpt2  19724  limcres  19726  cnplimc  19727  cnlimci  19729  elcpn  19773  uc1pval  20015  ig1pcl  20051  jensen  20780  nbgraop  21389  imsmet  22136  smcn  22147  iscbn  22319  zhmnrg  24304  ptpcon  24873  cvmscbv  24898  cvmshmeo  24911  cvmsss2  24914  cvmliftlem7  24931  cvmliftlem10  24934  cvmlift2lem11  24953  cvmlift2lem12  24954  ghomgrplem  25053  elfzp1b  25069  upixp  26321  sdclem1  26337  sstotbnd2  26373  prdsbnd2  26394  isprrngo  26550  isnacs3  26654  nacsfix  26656  mzpclall  26674  dnnumch1  27009  dnwech  27013  aomclem3  27021  aomclem8  27027  dfac11  27028  islmodfg  27035  frlmlbs  27117  islindf  27150  islinds2  27151  lindfind  27154  lindsind  27155  lindsind2  27157  lindfrn  27159  lindfmm  27165  lsslindf  27168  sblpnf  27407  rusbcALT  27507  climsuselem1  27600  climsuse  27601  stoweidlem31  27647  stoweidlem59  27675  dfateq12d  27860  swrdccatin12c  28028  isopos  29663  isatl  29782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2397  df-clel 2400
  Copyright terms: Public domain W3C validator