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

Theorem eleq12d 2539
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq2d.1
eleq12d.2
Assertion
Ref Expression
eleq12d

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3
21eleq2d 2527 . 2
3 eleq2d.1 . . 3
43eleq1d 2526 . 2
52, 4bitrd 253 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  e.wcel 1818
This theorem is referenced by:  neleq12d  2794  cbvraldva2  3088  cbvrexdva2  3089  cdeqel  3323  ru  3326  sbceqbid  3334  cbvralcsf  3466  cbvreucsf  3468  cbvrabcsf  3469  sbcel12  3823  sbcel12gOLD  3824  elvvuni  5065  elrnmpt1  5256  canth  6254  onnseq  7034  smoeq  7040  smores  7042  smores2  7044  iordsmo  7047  tz7.49  7129  nnaordr  7288  omsmolem  7321  fvixp  7494  cbvixp  7506  mptelixpg  7526  boxcutc  7532  ixpiunwdom  8038  elirr  8045  cantnflt  8112  oemapvali  8124  cantnflem1  8129  cantnf  8133  cantnfltOLD  8142  cantnflem1OLD  8152  cantnfOLD  8155  wemapwe  8160  wemapweOLD  8161  cnfcom3lem  8168  cnfcom3lemOLD  8176  infxpen  8413  dfac8alem  8431  dfac8clem  8434  ac5num  8438  acni2  8448  numacn  8451  acndom  8453  aceq3lem  8522  dfac5  8530  dfac9  8537  dfac13  8543  fin2i  8696  isfin2-2  8720  fin23lem27  8729  isfin3ds  8730  fin23lem17  8739  fin23lem39  8751  isf33lem  8767  isf34lem7  8780  isf34lem6  8781  fin1a2lem10  8810  fin1a2lem12  8812  hsmexlem4  8830  axcc2lem  8837  axcc3  8839  domtriomlem  8843  axdc2lem  8849  axdc3lem2  8852  axdc3lem3  8853  axdc3lem4  8854  axdc3  8855  axdc4lem  8856  axcclem  8858  ac6num  8880  ac6c4  8882  iundom2g  8936  fpwwe2  9042  pwfseqlem1  9057  pwfseqlem4a  9060  pwfseqlem4  9061  ltapi  9302  ltmpi  9303  eluzadd  11138  fzsubel  11748  elfzp1b  11784  axdc4uzlem  12092  wrd2ind  12703  smuval  14131  prdsbasprj  14869  xpsfrnel  14960  ismri2dad  15034  mreexd  15039  mreacs  15055  iscat  15069  iscatd  15070  iscatd2  15078  catcocl  15082  catpropd  15104  brssc  15183  issubc  15204  subcidcl  15213  subccocl  15214  isfunc  15233  isfuncd  15234  cofucl  15257  funcres2b  15266  fuciso  15344  yonedalem3  15549  yonffthlem  15551  ismgm  15873  ismndOLD  15926  ismndd  15943  eqgfval  16249  efgsdm  16748  efgsdmi  16750  efgsrel  16752  efgsp1  16755  efgsres  16756  dprdwdOLD2  17045  dprdfcl  17047  dprdwdOLD  17051  dprdfclOLD  17053  ablfaclem3  17138  isdrngd  17421  issrng  17499  issrngd  17510  islmodd  17518  islbs  17722  lbsind  17726  lbspropd  17745  islbs2  17800  lbsextlem4  17807  lbsextg  17808  zndvds  18588  isphl  18663  isphld  18689  phlpropd  18690  frlmlbs  18831  islindf  18847  islinds2  18848  lindfind  18851  lindsind  18852  lindsind2  18854  lindfrn  18856  lindfmm  18862  lsslindf  18865  mat1dimmul  18978  istps  19437  tpspropd  19441  eltpsg  19446  islp  19641  1stcelcls  19962  kgeni  20038  kgencn2  20058  ptpjpre1  20072  elptr2  20075  ptbasin  20078  ptbasfi  20082  ptpjcn  20112  ptpjopn  20113  ptcld  20114  ptcldmpt  20115  ptclsg  20116  ptcnp  20123  qtopval  20196  ptcmplem2  20553  ptcmplem3  20554  ptcmplem4  20555  istmd  20573  istgp  20576  tmdgsum  20594  istlm  20687  isusp  20764  prdsdsf  20870  prdsxmet  20872  isms  20952  mspropd  20977  setsxms  20982  setsms  20983  tmsxms  20989  tmsms  20990  isnrg  21169  tngnrg  21183  bcthlem2  21764  bcthlem3  21765  bcthlem4  21766  bcthlem5  21767  iscms  21784  cmspropd  21788  cmsss  21789  shft2rab  21919  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2lem5  21932  vitalilem2  22018  vitalilem3  22019  vitali  22022  limcfval  22276  limcmpt2  22288  limcres  22290  cnplimc  22291  cnlimci  22293  elcpn  22337  uc1pval  22540  ig1pcl  22576  jensen  23318  axtgcont  23866  tglngval  23938  ishlg  23986  mirbtwnb  24052  nbgraop  24423  nbgraopALT  24424  imsmet  25597  smcn  25608  iscbn  25780  sbceqbidf  27380  isslmd  27745  ispcmp  27860  zhmnrg  27948  ismntoplly  28003  eulerpartlemgvv  28315  eulerpart  28321  ptpcon  28678  cvmscbv  28703  cvmshmeo  28716  cvmsss2  28719  cvmliftlem7  28736  cvmliftlem10  28739  cvmlift2lem11  28758  cvmlift2lem12  28759  elmpps  28933  ghomgrplem  29029  ptrest  30048  upixp  30220  sdclem1  30236  sstotbnd2  30270  prdsbnd2  30291  isprrngo  30447  isnacs3  30642  nacsfix  30644  mzpclall  30659  dnnumch1  30990  dnwech  30994  aomclem3  31002  aomclem8  31007  dfac11  31008  islmodfg  31015  sblpnf  31190  rusbcALT  31346  climsuselem1  31613  climsuse  31614  cncfuni  31689  dvnprodlem1  31743  stoweidlem31  31813  stoweidlem59  31841  fourierdlem46  31935  fourierdlem62  31951  fourierdlem72  31961  fourierdlem79  31968  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem112  32001  dfateq12d  32214  ismgmd  32464  iscllaw  32513  islininds  33047  isopos  34905  isatl  35024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator