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

Theorem eleq12d 2724
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 2716 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq12d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2715 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  neleq12d  2930  cbvraldva2  3205  cbvrexdva2  3206  cdeqel  3464  ru  3467  sbceqbid  3475  cbvralcsf  3598  cbvreucsf  3600  cbvrabcsf  3601  sbcel12  4016  elvvuni  5213  elrnmpt1  5406  canth  6648  onnseq  7486  smoeq  7492  smores  7494  smores2  7496  iordsmo  7499  tz7.49  7585  nnaordr  7745  omsmolem  7778  fvixp  7955  cbvixp  7967  mptelixpg  7987  boxcutc  7993  ixpiunwdom  8537  elirr  8543  cantnflt  8607  oemapvali  8619  cantnflem1  8624  cantnf  8628  wemapwe  8632  cnfcom3lem  8638  infxpen  8875  dfac8alem  8890  dfac8clem  8893  ac5num  8897  acni2  8907  numacn  8910  acndom  8912  aceq3lem  8981  dfac5  8989  dfac9  8996  dfac13  9002  fin2i  9155  isfin2-2  9179  fin23lem27  9188  isfin3ds  9189  fin23lem17  9198  fin23lem39  9210  isf33lem  9226  isf34lem7  9239  isf34lem6  9240  fin1a2lem10  9269  fin1a2lem12  9271  hsmexlem4  9289  axcc2lem  9296  axcc3  9298  domtriomlem  9302  axdc2lem  9308  axdc3lem2  9311  axdc3lem3  9312  axdc3lem4  9313  axdc3  9314  axdc4lem  9315  axcclem  9317  ac6num  9339  ac6c4  9341  iundom2g  9400  fpwwe2  9503  pwfseqlem1  9518  pwfseqlem4a  9521  pwfseqlem4  9522  ltapi  9763  ltmpi  9764  eluzadd  11754  fzsubel  12415  elfzp1b  12455  axdc4uzlem  12822  wrd2ind  13523  smuval  15250  prdsbasprj  16179  xpsfrnel  16270  ismri2dad  16344  mreexd  16349  mreacs  16366  iscat  16380  iscatd  16381  iscatd2  16389  catcocl  16393  catpropd  16416  brssc  16521  issubc  16542  subcidcl  16551  subccocl  16552  isfunc  16571  isfuncd  16572  cofucl  16595  funcres2b  16604  fuciso  16682  yonedalem3  16967  yonffthlem  16969  ismgm  17290  issstrmgm  17299  ismndd  17360  eqgfval  17689  efgsdm  18189  efgsdmi  18191  efgsrel  18193  efgsp1  18196  efgsres  18197  dprdfcl  18458  ablfaclem3  18532  isdrngd  18820  issrng  18898  issrngd  18909  islmodd  18917  islbs  19124  lbsind  19128  lbspropd  19147  islbs2  19202  lbsextlem4  19209  lbsextg  19210  zndvds  19946  isphl  20021  isphld  20047  phlpropd  20048  frlmlbs  20184  islindf  20199  islinds2  20200  lindfind  20203  lindsind  20204  lindsind2  20206  lindfrn  20208  lindfmm  20214  lsslindf  20217  mat1dimmul  20330  istps  20786  tpspropd  20790  eltpsg  20795  islp  20992  1stcelcls  21312  kgeni  21388  kgencn2  21408  ptpjpre1  21422  elptr2  21425  ptbasin  21428  ptbasfi  21432  ptpjcn  21462  ptpjopn  21463  ptcld  21464  ptcldmpt  21465  ptclsg  21466  ptcnp  21473  qtopval  21546  ptcmplem2  21904  ptcmplem3  21905  ptcmplem4  21906  istmd  21925  istgp  21928  tmdgsum  21946  istlm  22035  isusp  22112  prdsdsf  22219  prdsxmet  22221  isms  22301  mspropd  22326  setsxms  22331  setsms  22332  tmsxms  22338  tmsms  22339  isnrg  22511  tngnrg  22525  bcthlem2  23168  bcthlem3  23169  bcthlem4  23170  bcthlem5  23171  iscms  23188  cmspropd  23192  cmsss  23193  shft2rab  23322  ovolicc2lem3  23333  ovolicc2lem4  23334  ovolicc2lem5  23335  vitalilem2  23423  vitalilem3  23424  vitali  23427  limcfval  23681  limcmpt2  23693  limcres  23695  cnplimc  23696  cnlimci  23698  elcpn  23742  uc1pval  23944  ig1pcl  23980  jensen  24760  axtgcont  25413  tglngval  25491  ishlg  25542  mirbtwnb  25612  islnopp  25676  outpasch  25692  colhp  25707  trgcopy  25741  trgcopyeu  25743  dfcgra2  25766  acopyeu  25770  isinag  25774  tgasa1  25784  wlkp1lem3  26628  umgrwwlks2on  26923  clwwlknon1  27072  imsmet  27674  smcn  27681  iscbn  27848  sbceqbidf  29449  isslmd  29883  submateq  30003  lmatcl  30010  ispcmp  30052  zhmnrg  30139  ismntoplly  30197  inelpisys  30345  sigapildsys  30353  fiunelcarsg  30506  eulerpartlemgvv  30566  eulerpart  30572  ptpconn  31341  cvmscbv  31366  cvmshmeo  31379  cvmsss2  31382  cvmliftlem7  31399  cvmliftlem10  31402  cvmlift2lem11  31421  cvmlift2lem12  31422  elmpps  31596  bj-ismoore  33184  csbfinxpg  33355  lindsenlbs  33534  ptrest  33538  upixp  33654  sdclem1  33669  sstotbnd2  33703  prdsbnd2  33724  isprrngo  33979  isopos  34785  isatl  34904  isnacs3  37590  nacsfix  37592  mzpclall  37607  dnnumch1  37931  dnwech  37935  aomclem3  37943  aomclem8  37948  dfac11  37949  islmodfg  37956  rfovcnvf1od  38615  sblpnf  38826  rusbcALT  38957  sbcel12gOLD  39071  choicefi  39706  climsuselem1  40157  climsuse  40158  cncfuni  40417  dvnprodlem1  40479  stoweidlem31  40566  stoweidlem59  40594  fourierdlem46  40687  fourierdlem62  40703  fourierdlem72  40713  fourierdlem79  40720  fourierdlem88  40729  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem112  40753  qndenserrnbllem  40832  ioorrnopnlem  40842  ioorrnopn  40843  ioorrnopnxr  40845  issal  40852  subsaliuncllem  40893  subsaliuncl  40894  subsalsal  40895  sge0tsms  40915  sge0iunmpt  40953  sge0seq  40981  ovnsubaddlem1  41105  ovnsubaddlem2  41106  hoidmvlelem3  41132  hoidmvlelem4  41133  rrnmbl  41149  hoiqssbllem3  41159  hspmbl  41164  hoimbl  41166  issmflem  41257  issmfd  41265  issmfdf  41267  smfpimltmpt  41276  issmfled  41287  smfpimltxrmpt  41288  smfmbfcex  41289  issmfgtd  41290  smflimlem1  41300  smflimlem2  41301  smflimlem3  41302  smflimlem6  41305  smfpimgtmpt  41310  smfpimgtxrmpt  41313  smfres  41318  smfco  41330  smfpimcclem  41334  smfpimcc  41335  dfateq12d  41530  ismgmd  42101  iscllaw  42150  islininds  42560
  Copyright terms: Public domain W3C validator