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

Theorem eleq12d 2844
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq12d.1 (𝜑𝐴 = 𝐵)
eleq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
eleq12d (𝜑 → (𝐴𝐶𝐵𝐷))

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3 (𝜑𝐶 = 𝐷)
21eleq2d 2836 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq12d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2835 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1631  wcel 2145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-clel 2767
This theorem is referenced by:  neleq12d  3050  cbvraldva2  3324  cbvrexdva2  3325  cdeqel  3583  ru  3586  sbceqbid  3594  cbvralcsf  3714  cbvreucsf  3716  cbvrabcsf  3717  sbcel12  4127  elvvuni  5319  elrnmpt1  5512  canth  6751  onnseq  7594  smoeq  7600  smores  7602  smores2  7604  iordsmo  7607  tz7.49  7693  nnaordr  7854  omsmolem  7887  fvixp  8067  cbvixp  8079  mptelixpg  8099  boxcutc  8105  ixpiunwdom  8652  elirr  8658  cantnflt  8733  oemapvali  8745  cantnflem1  8750  cantnf  8754  wemapwe  8758  cnfcom3lem  8764  infxpen  9037  dfac8alem  9052  dfac8clem  9055  ac5num  9059  acni2  9069  numacn  9072  acndom  9074  aceq3lem  9143  dfac5  9151  dfac9  9160  dfac13  9166  fin2i  9319  isfin2-2  9343  fin23lem27  9352  isfin3ds  9353  fin23lem17  9362  fin23lem39  9374  isf33lem  9390  isf34lem7  9403  isf34lem6  9404  fin1a2lem10  9433  fin1a2lem12  9435  hsmexlem4  9453  axcc2lem  9460  axcc3  9462  domtriomlem  9466  axdc2lem  9472  axdc3lem2  9475  axdc3lem3  9476  axdc3lem4  9477  axdc3  9478  axdc4lem  9479  axcclem  9481  ac6num  9503  ac6c4  9505  iundom2g  9564  fpwwe2  9667  pwfseqlem1  9682  pwfseqlem4a  9685  pwfseqlem4  9686  ltapi  9927  ltmpi  9928  eluzadd  11917  fzsubel  12584  elfzp1b  12624  axdc4uzlem  12990  wrd2ind  13686  smuval  15411  prdsbasprj  16340  xpsfrnel  16431  ismri2dad  16505  mreexd  16510  mreacs  16526  iscat  16540  iscatd  16541  iscatd2  16549  catcocl  16553  catpropd  16576  brssc  16681  issubc  16702  subcidcl  16711  subccocl  16712  isfunc  16731  isfuncd  16732  cofucl  16755  funcres2b  16764  fuciso  16842  yonedalem3  17128  yonffthlem  17130  ismgm  17451  issstrmgm  17460  ismndd  17521  eqgfval  17850  efgsdm  18350  efgsdmi  18352  efgsrel  18354  efgsp1  18357  efgsres  18358  dprdfcl  18620  ablfaclem3  18694  isdrngd  18982  issrng  19060  issrngd  19071  islmodd  19079  islbs  19289  lbsind  19293  lbspropd  19312  islbs2  19369  lbsextlem4  19376  lbsextg  19377  zndvds  20113  isphl  20190  isphld  20216  phlpropd  20217  frlmlbs  20353  islindf  20368  islinds2  20369  lindfind  20372  lindsind  20373  lindsind2  20375  lindfrn  20377  lindfmm  20383  lsslindf  20386  mat1dimmul  20500  istps  20959  tpspropd  20963  eltpsg  20968  islp  21165  1stcelcls  21485  kgeni  21561  kgencn2  21581  ptpjpre1  21595  elptr2  21598  ptbasin  21601  ptbasfi  21605  ptpjcn  21635  ptpjopn  21636  ptcld  21637  ptcldmpt  21638  ptclsg  21639  ptcnp  21646  qtopval  21719  ptcmplem2  22077  ptcmplem3  22078  ptcmplem4  22079  istmd  22098  istgp  22101  tmdgsum  22119  istlm  22208  isusp  22285  prdsdsf  22392  prdsxmet  22394  isms  22474  mspropd  22499  setsxms  22504  setsms  22505  tmsxms  22511  tmsms  22512  isnrg  22684  tngnrg  22698  bcthlem2  23341  bcthlem3  23342  bcthlem4  23343  bcthlem5  23344  iscms  23361  cmspropd  23365  cmsss  23366  shft2rab  23496  ovolicc2lem3  23507  ovolicc2lem4  23508  ovolicc2lem5  23509  vitalilem2  23597  vitalilem3  23598  vitali  23601  limcfval  23856  limcmpt2  23868  limcres  23870  cnplimc  23871  cnlimci  23873  elcpn  23917  uc1pval  24119  ig1pcl  24155  jensen  24936  axtgcont  25589  tglngval  25667  ishlg  25718  mirbtwnb  25788  islnopp  25852  outpasch  25868  colhp  25883  trgcopy  25917  trgcopyeu  25919  dfcgra2  25942  acopyeu  25946  isinag  25950  tgasa1  25960  wlkp1lem3  26807  umgrwwlks2on  27105  clwwlknon1  27272  clwwlknonclwlknonf1o  27549  clwwlknonclwlknonf1oOLD  27551  imsmet  27886  smcn  27893  iscbn  28060  sbceqbidf  29661  isslmd  30095  submateq  30215  lmatcl  30222  ispcmp  30264  zhmnrg  30351  ismntoplly  30409  inelpisys  30557  sigapildsys  30565  fiunelcarsg  30718  eulerpartlemgvv  30778  eulerpart  30784  ptpconn  31553  cvmscbv  31578  cvmshmeo  31591  cvmsss2  31594  cvmliftlem7  31611  cvmliftlem10  31614  cvmlift2lem11  31633  cvmlift2lem12  31634  elmpps  31808  bj-ismoore  33391  csbfinxpg  33562  lindsenlbs  33737  ptrest  33741  upixp  33856  sdclem1  33871  sstotbnd2  33905  prdsbnd2  33926  isprrngo  34181  isopos  34989  isatl  35108  isnacs3  37799  nacsfix  37801  mzpclall  37816  dnnumch1  38140  dnwech  38144  aomclem3  38152  aomclem8  38157  dfac11  38158  islmodfg  38165  rfovcnvf1od  38824  sblpnf  39035  rusbcALT  39166  sbcel12gOLD  39279  choicefi  39910  climsuselem1  40357  climsuse  40358  cncfuni  40617  dvnprodlem1  40679  stoweidlem31  40765  stoweidlem59  40793  fourierdlem46  40886  fourierdlem62  40902  fourierdlem72  40912  fourierdlem79  40919  fourierdlem88  40928  fourierdlem89  40929  fourierdlem90  40930  fourierdlem91  40931  fourierdlem112  40952  qndenserrnbllem  41031  ioorrnopnlem  41041  ioorrnopn  41042  ioorrnopnxr  41044  issal  41051  subsaliuncllem  41092  subsaliuncl  41093  subsalsal  41094  sge0tsms  41114  sge0iunmpt  41152  sge0seq  41180  ovnsubaddlem1  41304  ovnsubaddlem2  41305  hoidmvlelem3  41331  hoidmvlelem4  41332  rrnmbl  41348  hoiqssbllem3  41358  hspmbl  41363  hoimbl  41365  issmflem  41456  issmfd  41464  issmfdf  41466  smfpimltmpt  41475  issmfled  41486  smfpimltxrmpt  41487  smfmbfcex  41488  issmfgtd  41489  smflimlem1  41499  smflimlem2  41500  smflimlem3  41501  smflimlem6  41504  smfpimgtmpt  41509  smfpimgtxrmpt  41512  smfres  41517  smfco  41529  smfpimcclem  41533  smfpimcc  41534  dfateq12d  41729  ismgmd  42304  iscllaw  42353  islininds  42763
  Copyright terms: Public domain W3C validator