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

Theorem eleq12d 2693
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 2685 . 2 (𝜑 → (𝐴𝐶𝐴𝐷))
3 eleq12d.1 . . 3 (𝜑𝐴 = 𝐵)
43eleq1d 2684 . 2 (𝜑 → (𝐴𝐷𝐵𝐷))
52, 4bitrd 268 1 (𝜑 → (𝐴𝐶𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481  wcel 1988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-clel 2616
This theorem is referenced by:  neleq12d  2898  cbvraldva2  3170  cbvrexdva2  3171  cdeqel  3425  ru  3428  sbceqbid  3436  cbvralcsf  3558  cbvreucsf  3560  cbvrabcsf  3561  sbcel12  3974  elvvuni  5169  elrnmpt1  5363  canth  6593  onnseq  7426  smoeq  7432  smores  7434  smores2  7436  iordsmo  7439  tz7.49  7525  nnaordr  7685  omsmolem  7718  fvixp  7898  cbvixp  7910  mptelixpg  7930  boxcutc  7936  ixpiunwdom  8481  elirr  8490  cantnflt  8554  oemapvali  8566  cantnflem1  8571  cantnf  8575  wemapwe  8579  cnfcom3lem  8585  infxpen  8822  dfac8alem  8837  dfac8clem  8840  ac5num  8844  acni2  8854  numacn  8857  acndom  8859  aceq3lem  8928  dfac5  8936  dfac9  8943  dfac13  8949  fin2i  9102  isfin2-2  9126  fin23lem27  9135  isfin3ds  9136  fin23lem17  9145  fin23lem39  9157  isf33lem  9173  isf34lem7  9186  isf34lem6  9187  fin1a2lem10  9216  fin1a2lem12  9218  hsmexlem4  9236  axcc2lem  9243  axcc3  9245  domtriomlem  9249  axdc2lem  9255  axdc3lem2  9258  axdc3lem3  9259  axdc3lem4  9260  axdc3  9261  axdc4lem  9262  axcclem  9264  ac6num  9286  ac6c4  9288  iundom2g  9347  fpwwe2  9450  pwfseqlem1  9465  pwfseqlem4a  9468  pwfseqlem4  9469  ltapi  9710  ltmpi  9711  eluzadd  11701  fzsubel  12362  elfzp1b  12401  axdc4uzlem  12765  wrd2ind  13459  smuval  15184  prdsbasprj  16113  xpsfrnel  16204  ismri2dad  16278  mreexd  16283  mreacs  16300  iscat  16314  iscatd  16315  iscatd2  16323  catcocl  16327  catpropd  16350  brssc  16455  issubc  16476  subcidcl  16485  subccocl  16486  isfunc  16505  isfuncd  16506  cofucl  16529  funcres2b  16538  fuciso  16616  yonedalem3  16901  yonffthlem  16903  ismgm  17224  issstrmgm  17233  ismndd  17294  eqgfval  17623  efgsdm  18124  efgsdmi  18126  efgsrel  18128  efgsp1  18131  efgsres  18132  dprdfcl  18393  ablfaclem3  18467  isdrngd  18753  issrng  18831  issrngd  18842  islmodd  18850  islbs  19057  lbsind  19061  lbspropd  19080  islbs2  19135  lbsextlem4  19142  lbsextg  19143  zndvds  19879  isphl  19954  isphld  19980  phlpropd  19981  frlmlbs  20117  islindf  20132  islinds2  20133  lindfind  20136  lindsind  20137  lindsind2  20139  lindfrn  20141  lindfmm  20147  lsslindf  20150  mat1dimmul  20263  istps  20719  tpspropd  20723  eltpsg  20728  islp  20925  1stcelcls  21245  kgeni  21321  kgencn2  21341  ptpjpre1  21355  elptr2  21358  ptbasin  21361  ptbasfi  21365  ptpjcn  21395  ptpjopn  21396  ptcld  21397  ptcldmpt  21398  ptclsg  21399  ptcnp  21406  qtopval  21479  ptcmplem2  21838  ptcmplem3  21839  ptcmplem4  21840  istmd  21859  istgp  21862  tmdgsum  21880  istlm  21969  isusp  22046  prdsdsf  22153  prdsxmet  22155  isms  22235  mspropd  22260  setsxms  22265  setsms  22266  tmsxms  22272  tmsms  22273  isnrg  22445  tngnrg  22459  bcthlem2  23103  bcthlem3  23104  bcthlem4  23105  bcthlem5  23106  iscms  23123  cmspropd  23127  cmsss  23128  shft2rab  23257  ovolicc2lem3  23268  ovolicc2lem4  23269  ovolicc2lem5  23270  vitalilem2  23359  vitalilem3  23360  vitali  23363  limcfval  23617  limcmpt2  23629  limcres  23631  cnplimc  23632  cnlimci  23634  elcpn  23678  uc1pval  23880  ig1pcl  23916  jensen  24696  axtgcont  25349  tglngval  25427  ishlg  25478  mirbtwnb  25548  islnopp  25612  outpasch  25628  colhp  25643  trgcopy  25677  trgcopyeu  25679  dfcgra2  25702  acopyeu  25706  isinag  25710  tgasa1  25720  wlkp1lem3  26553  umgrwwlks2on  26831  imsmet  27516  smcn  27523  iscbn  27690  sbceqbidf  29293  isslmd  29729  submateq  29849  lmatcl  29856  ispcmp  29898  zhmnrg  29985  ismntoplly  30043  inelpisys  30191  sigapildsys  30199  fiunelcarsg  30352  eulerpartlemgvv  30412  eulerpart  30418  ptpconn  31189  cvmscbv  31214  cvmshmeo  31227  cvmsss2  31230  cvmliftlem7  31247  cvmliftlem10  31250  cvmlift2lem11  31269  cvmlift2lem12  31270  elmpps  31444  bj-ismoore  33034  csbfinxpg  33196  lindsenlbs  33375  ptrest  33379  upixp  33495  sdclem1  33510  sstotbnd2  33544  prdsbnd2  33565  isprrngo  33820  isopos  34286  isatl  34405  isnacs3  37092  nacsfix  37094  mzpclall  37109  dnnumch1  37433  dnwech  37437  aomclem3  37445  aomclem8  37450  dfac11  37451  islmodfg  37458  rfovcnvf1od  38118  sblpnf  38329  rusbcALT  38460  sbcel12gOLD  38574  choicefi  39208  climsuselem1  39639  climsuse  39640  cncfuni  39862  dvnprodlem1  39924  stoweidlem31  40011  stoweidlem59  40039  fourierdlem46  40132  fourierdlem62  40148  fourierdlem72  40158  fourierdlem79  40165  fourierdlem88  40174  fourierdlem89  40175  fourierdlem90  40176  fourierdlem91  40177  fourierdlem112  40198  qndenserrnbllem  40277  ioorrnopnlem  40287  ioorrnopn  40288  ioorrnopnxr  40290  issal  40297  subsaliuncllem  40338  subsaliuncl  40339  subsalsal  40340  sge0tsms  40360  sge0iunmpt  40398  sge0seq  40426  ovnsubaddlem1  40547  ovnsubaddlem2  40548  hoidmvlelem3  40574  hoidmvlelem4  40575  rrnmbl  40591  hoiqssbllem3  40601  hspmbl  40606  hoimbl  40608  issmflem  40699  issmfd  40707  issmfdf  40709  smfpimltmpt  40718  issmfled  40729  smfpimltxrmpt  40730  smfmbfcex  40731  issmfgtd  40732  smflimlem1  40742  smflimlem2  40743  smflimlem3  40744  smflimlem6  40747  smfpimgtmpt  40752  smfpimgtxrmpt  40755  smfres  40760  smfco  40772  smfpimcclem  40776  smfpimcc  40777  dfateq12d  40972  ismgmd  41541  iscllaw  41590  islininds  42000
  Copyright terms: Public domain W3C validator