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

Theorem eleq12d 2681
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 2672 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq12d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2671 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 266 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  neleq12d  2886  cbvraldva2  3150  cbvrexdva2  3151  cdeqel  3397  ru  3400  sbceqbid  3408  cbvralcsf  3530  cbvreucsf  3532  cbvrabcsf  3533  sbcel12  3934  elvvuni  5091  elrnmpt1  5281  canth  6485  onnseq  7305  smoeq  7311  smores  7313  smores2  7315  iordsmo  7318  tz7.49  7404  nnaordr  7564  omsmolem  7597  fvixp  7776  cbvixp  7788  mptelixpg  7808  boxcutc  7814  ixpiunwdom  8356  elirr  8365  cantnflt  8429  oemapvali  8441  cantnflem1  8446  cantnf  8450  wemapwe  8454  cnfcom3lem  8460  infxpen  8697  dfac8alem  8712  dfac8clem  8715  ac5num  8719  acni2  8729  numacn  8732  acndom  8734  aceq3lem  8803  dfac5  8811  dfac9  8818  dfac13  8824  fin2i  8977  isfin2-2  9001  fin23lem27  9010  isfin3ds  9011  fin23lem17  9020  fin23lem39  9032  isf33lem  9048  isf34lem7  9061  isf34lem6  9062  fin1a2lem10  9091  fin1a2lem12  9093  hsmexlem4  9111  axcc2lem  9118  axcc3  9120  domtriomlem  9124  axdc2lem  9130  axdc3lem2  9133  axdc3lem3  9134  axdc3lem4  9135  axdc3  9136  axdc4lem  9137  axcclem  9139  ac6num  9161  ac6c4  9163  iundom2g  9218  fpwwe2  9321  pwfseqlem1  9336  pwfseqlem4a  9339  pwfseqlem4  9340  ltapi  9581  ltmpi  9582  eluzadd  11550  fzsubel  12205  elfzp1b  12243  axdc4uzlem  12601  wrd2ind  13277  smuval  14989  prdsbasprj  15903  xpsfrnel  15994  ismri2dad  16068  mreexd  16073  mreacs  16090  iscat  16104  iscatd  16105  iscatd2  16113  catcocl  16117  catpropd  16140  brssc  16245  issubc  16266  subcidcl  16275  subccocl  16276  isfunc  16295  isfuncd  16296  cofucl  16319  funcres2b  16328  fuciso  16406  yonedalem3  16691  yonffthlem  16693  ismgm  17014  issstrmgm  17023  ismndd  17084  eqgfval  17413  efgsdm  17914  efgsdmi  17916  efgsrel  17918  efgsp1  17921  efgsres  17922  dprdfcl  18183  ablfaclem3  18257  isdrngd  18543  issrng  18621  issrngd  18632  islmodd  18640  islbs  18845  lbsind  18849  lbspropd  18868  islbs2  18923  lbsextlem4  18930  lbsextg  18931  zndvds  19664  isphl  19739  isphld  19765  phlpropd  19766  frlmlbs  19902  islindf  19917  islinds2  19918  lindfind  19921  lindsind  19922  lindsind2  19924  lindfrn  19926  lindfmm  19932  lsslindf  19935  mat1dimmul  20048  istps  20498  tpspropd  20502  eltpsg  20507  islp  20701  1stcelcls  21021  kgeni  21097  kgencn2  21117  ptpjpre1  21131  elptr2  21134  ptbasin  21137  ptbasfi  21141  ptpjcn  21171  ptpjopn  21172  ptcld  21173  ptcldmpt  21174  ptclsg  21175  ptcnp  21182  qtopval  21255  ptcmplem2  21614  ptcmplem3  21615  ptcmplem4  21616  istmd  21635  istgp  21638  tmdgsum  21656  istlm  21745  isusp  21822  prdsdsf  21929  prdsxmet  21931  isms  22011  mspropd  22036  setsxms  22041  setsms  22042  tmsxms  22048  tmsms  22049  isnrg  22221  tngnrg  22235  bcthlem2  22874  bcthlem3  22875  bcthlem4  22876  bcthlem5  22877  iscms  22894  cmspropd  22898  cmsss  22899  shft2rab  23027  ovolicc2lem3  23038  ovolicc2lem4  23039  ovolicc2lem5  23040  vitalilem2  23128  vitalilem3  23129  vitali  23132  limcfval  23386  limcmpt2  23398  limcres  23400  cnplimc  23401  cnlimci  23403  elcpn  23447  uc1pval  23647  ig1pcl  23683  jensen  24459  axtgcont  25112  tglngval  25191  ishlg  25242  mirbtwnb  25312  islnopp  25376  outpasch  25392  colhp  25407  trgcopy  25441  trgcopyeu  25443  dfcgra2  25466  acopyeu  25470  isinag  25474  tgasa1  25484  nbgraop  25745  nbgraopALT  25746  imsmet  26723  smcn  26730  iscbn  26897  sbceqbidf  28498  isslmd  28879  submateq  28996  lmatcl  29003  ispcmp  29045  zhmnrg  29132  ismntoplly  29190  inelpisys  29337  sigapildsys  29345  fiunelcarsg  29498  eulerpartlemgvv  29558  eulerpart  29564  ptpcon  30262  cvmscbv  30287  cvmshmeo  30300  cvmsss2  30303  cvmliftlem7  30320  cvmliftlem10  30323  cvmlift2lem11  30342  cvmlift2lem12  30343  elmpps  30517  csbfinxpg  32184  lindsenlbs  32357  ptrest  32361  upixp  32477  sdclem1  32492  sstotbnd2  32526  prdsbnd2  32547  isprrngo  32802  isopos  33268  isatl  33387  isnacs3  36074  nacsfix  36076  mzpclall  36091  dnnumch1  36415  dnwech  36419  aomclem3  36427  aomclem8  36432  dfac11  36433  islmodfg  36440  rfovcnvf1od  37101  sblpnf  37314  rusbcALT  37445  sbcel12gOLD  37558  choicefi  38170  climsuselem1  38457  climsuse  38458  cncfuni  38555  dvnprodlem1  38619  stoweidlem31  38707  stoweidlem59  38735  fourierdlem46  38828  fourierdlem62  38844  fourierdlem72  38854  fourierdlem79  38861  fourierdlem88  38870  fourierdlem89  38871  fourierdlem90  38872  fourierdlem91  38873  fourierdlem112  38894  qndenserrnbllem  38973  ioorrnopnlem  38983  ioorrnopn  38984  ioorrnopnxr  38986  issal  38993  subsaliuncllem  39034  subsaliuncl  39035  subsalsal  39036  sge0tsms  39056  sge0iunmpt  39094  sge0seq  39122  ovnsubaddlem1  39243  ovnsubaddlem2  39244  hoidmvlelem3  39270  hoidmvlelem4  39271  rrnmbl  39287  hoiqssbllem3  39297  hspmbl  39302  hoimbl  39304  issmflem  39396  issmfd  39404  issmfdf  39407  smfpimltmpt  39416  issmfled  39427  smfpimltxrmpt  39428  smfmbfcex  39429  issmfgtd  39430  smflimlem1  39440  smflimlem2  39441  smflimlem3  39442  smflimlem6  39445  smfpimgtmpt  39450  smfpimgtxrmpt  39453  smfres  39458  smfco  39470  dfateq12d  39642  1wlkp1lem3  40865  umgrwwlks2on  41142  ismgmd  41547  iscllaw  41596  islininds  42010
  Copyright terms: Public domain W3C validator