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

Theorem eleq12d 2904
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 2895 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq12d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2894 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 280 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  neleq12d  3124  cbvraldva2  3454  cbvrexdva2  3455  cbvrexdva2OLD  3456  cdeqel  3764  ru  3768  sbceqbid  3776  cbvrabcsfw  3921  cbvralcsf  3922  cbvreucsf  3924  cbvrabcsf  3925  sbcel12  4357  elvvuni  5621  elrnmpt1  5823  canth  7100  onnseq  7970  smoeq  7976  smores  7978  smores2  7980  iordsmo  7983  tz7.49  8070  nnaordr  8235  omsmolem  8269  fvixp  8454  cbvixp  8466  mptelixpg  8487  boxcutc  8493  ixpiunwdom  9043  elirr  9049  cantnflt  9123  oemapvali  9135  cantnflem1  9140  cantnf  9144  wemapwe  9148  cnfcom3lem  9154  infxpen  9428  dfac8alem  9443  dfac8clem  9446  ac5num  9450  acni2  9460  numacn  9463  acndom  9465  aceq3lem  9534  dfac5  9542  dfac9  9550  dfac13  9556  fin2i  9705  isfin2-2  9729  fin23lem27  9738  isfin3ds  9739  fin23lem17  9748  fin23lem39  9760  isf33lem  9776  isf34lem7  9789  isf34lem6  9790  fin1a2lem10  9819  fin1a2lem12  9821  hsmexlem4  9839  axcc2lem  9846  axcc3  9848  domtriomlem  9852  axdc2lem  9858  axdc3lem2  9861  axdc3lem3  9862  axdc3lem4  9863  axdc3  9864  axdc4lem  9865  axcclem  9867  ac6num  9889  ac6c4  9891  iundom2g  9950  fpwwe2  10053  pwfseqlem1  10068  pwfseqlem4a  10071  pwfseqlem4  10072  ltapi  10313  ltmpi  10314  eluzadd  12261  fzsubel  12931  elfzp1b  12972  axdc4uzlem  13339  wrd2ind  14073  smuval  15818  prdsbasprj  16733  xpsfrnel  16823  ismri2dad  16896  mreexd  16901  mreacs  16917  iscat  16931  iscatd  16932  iscatd2  16940  catcocl  16944  catpropd  16967  brssc  17072  issubc  17093  subcidcl  17102  subccocl  17103  isfunc  17122  isfuncd  17123  cofucl  17146  funcres2b  17155  fuciso  17233  yonedalem3  17518  yonffthlem  17520  ismgm  17841  issstrmgm  17851  ismndd  17921  eqgfval  18266  efgsdm  18785  efgsdmi  18787  efgsrel  18789  efgsp1  18792  efgsres  18793  dprdfcl  19064  ablfaclem3  19138  isdrngd  19456  issrng  19550  issrngd  19561  islmodd  19569  islbs  19777  lbsind  19781  lbspropd  19800  islbs2  19855  lbsextlem4  19862  lbsextg  19863  zndvds  20624  isphl  20700  isphld  20726  phlpropd  20727  frlmlbs  20869  islindf  20884  islinds2  20885  lindfind  20888  lindsind  20889  lindsind2  20891  lindfrn  20893  lindfmm  20899  lsslindf  20902  mat1dimmul  21013  istps  21470  tpspropd  21474  eltpsg  21479  islp  21676  1stcelcls  21997  kgeni  22073  kgencn2  22093  ptpjpre1  22107  elptr2  22110  ptbasin  22113  ptbasfi  22117  ptpjcn  22147  ptpjopn  22148  ptcld  22149  ptcldmpt  22150  ptclsg  22151  ptcnp  22158  qtopval  22231  ptcmplem2  22589  ptcmplem3  22590  ptcmplem4  22591  istmd  22610  istgp  22613  tmdgsum  22631  istlm  22720  isusp  22797  prdsdsf  22904  prdsxmet  22906  isms  22986  mspropd  23011  setsxms  23016  setsms  23017  tmsxms  23023  tmsms  23024  isnrg  23196  tngnrg  23210  bcthlem2  23855  bcthlem3  23856  bcthlem4  23857  bcthlem5  23858  iscms  23875  cmspropd  23879  cmssmscld  23880  cmsss  23881  shft2rab  24036  ovolicc2lem3  24047  ovolicc2lem4  24048  ovolicc2lem5  24049  vitalilem2  24137  vitalilem3  24138  vitali  24141  limcfval  24397  limcmpt2  24409  limcres  24411  cnplimc  24412  cnlimci  24414  elcpn  24458  uc1pval  24660  ig1pcl  24696  jensen  25493  axtgcont  26182  tglngval  26264  ishlg  26315  mirbtwnb  26385  trgcopy  26517  trgcopyeu  26519  acopyeu  26547  isinagd  26552  tgasa1  26571  wlkp1lem3  27384  umgrwwlks2on  27663  clwwlknon1  27803  clwwlknonclwlknonf1o  28068  imsmet  28395  smcn  28402  iscbn  28568  sbceqbidf  30177  fnpreimac  30344  isslmd  30757  0nellinds  30862  lindssn  30866  lindfpropd  30869  lbslsat  30913  lindsunlem  30919  brfldext  30936  submateq  30973  lmatcl  30980  ispcmp  31020  zhmnrg  31107  ismntoplly  31165  inelpisys  31312  sigapildsys  31320  fiunelcarsg  31473  eulerpartlemgvv  31533  eulerpart  31539  ptpconn  32377  cvmscbv  32402  cvmshmeo  32415  cvmsss2  32418  cvmliftlem7  32435  cvmliftlem10  32438  cvmlift2lem11  32457  cvmlift2lem12  32458  satffunlem1lem1  32546  satffunlem2lem1  32548  sategoelfvb  32563  prv1n  32575  elmpps  32717  currysetlem  34153  currysetlem1  34155  bj-ismoore  34291  csbfinxpg  34551  pibt2  34580  lindsadd  34766  lindsenlbs  34768  ptrest  34772  upixp  34885  sdclem1  34899  sstotbnd2  34933  prdsbnd2  34954  isprrngo  35209  isopos  36196  isatl  36315  isnacs3  39185  nacsfix  39187  mzpclall  39202  dnnumch1  39522  dnwech  39526  aomclem3  39534  aomclem8  39539  dfac11  39540  islmodfg  39547  rfovcnvf1od  40228  ismnu  40474  sblpnf  40519  rusbcALT  40648  choicefi  41339  climsuselem1  41764  climsuse  41765  cncfuni  42045  dvnprodlem1  42107  stoweidlem31  42193  stoweidlem59  42221  fourierdlem46  42314  fourierdlem62  42330  fourierdlem72  42340  fourierdlem79  42347  fourierdlem88  42356  fourierdlem89  42357  fourierdlem90  42358  fourierdlem91  42359  fourierdlem112  42380  qndenserrnbllem  42456  ioorrnopnlem  42466  ioorrnopn  42467  ioorrnopnxr  42469  issal  42476  subsaliuncllem  42517  subsaliuncl  42518  subsalsal  42519  sge0tsms  42539  sge0iunmpt  42577  sge0seq  42605  ovnsubaddlem1  42729  ovnsubaddlem2  42730  hoidmvlelem3  42756  hoidmvlelem4  42757  rrnmbl  42773  hoiqssbllem3  42783  hspmbl  42788  hoimbl  42790  issmflem  42881  issmfd  42889  issmfdf  42891  smfpimltmpt  42900  issmfled  42911  smfpimltxrmpt  42912  smfmbfcex  42913  issmfgtd  42914  smflimlem1  42924  smflimlem2  42925  smflimlem3  42926  smflimlem6  42929  smfpimgtmpt  42934  smfpimgtxrmpt  42937  smfres  42942  smfco  42954  smfpimcclem  42958  smfpimcc  42959  dfateq12d  43202  ismgmd  43920  iscllaw  44024  islininds  44429
  Copyright terms: Public domain W3C validator