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

Theorem eleq12d 2543
Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)
Hypotheses
Ref Expression
eleq12d.1  |-  ( ph  ->  A  =  B )
eleq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
eleq12d  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )

Proof of Theorem eleq12d
StepHypRef Expression
1 eleq12d.2 . . 3  |-  ( ph  ->  C  =  D )
21eleq2d 2534 . 2  |-  ( ph  ->  ( A  e.  C  <->  A  e.  D ) )
3 eleq12d.1 . . 3  |-  ( ph  ->  A  =  B )
43eleq1d 2533 . 2  |-  ( ph  ->  ( A  e.  D  <->  B  e.  D ) )
52, 4bitrd 261 1  |-  ( ph  ->  ( A  e.  C  <->  B  e.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452    e. wcel 1904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-cleq 2464  df-clel 2467
This theorem is referenced by:  neleq12d  2747  cbvraldva2  3009  cbvrexdva2  3010  cdeqel  3251  ru  3254  sbceqbid  3262  cbvralcsf  3381  cbvreucsf  3383  cbvrabcsf  3384  sbcel12  3776  elvvuni  4900  elrnmpt1  5089  canth  6267  onnseq  7081  smoeq  7087  smores  7089  smores2  7091  iordsmo  7094  tz7.49  7180  nnaordr  7339  omsmolem  7372  fvixp  7545  cbvixp  7557  mptelixpg  7577  boxcutc  7583  ixpiunwdom  8124  elirr  8131  cantnflt  8195  oemapvali  8207  cantnflem1  8212  cantnf  8216  wemapwe  8220  cnfcom3lem  8226  infxpen  8463  dfac8alem  8478  dfac8clem  8481  ac5num  8485  acni2  8495  numacn  8498  acndom  8500  aceq3lem  8569  dfac5  8577  dfac9  8584  dfac13  8590  fin2i  8743  isfin2-2  8767  fin23lem27  8776  isfin3ds  8777  fin23lem17  8786  fin23lem39  8798  isf33lem  8814  isf34lem7  8827  isf34lem6  8828  fin1a2lem10  8857  fin1a2lem12  8859  hsmexlem4  8877  axcc2lem  8884  axcc3  8886  domtriomlem  8890  axdc2lem  8896  axdc3lem2  8899  axdc3lem3  8900  axdc3lem4  8901  axdc3  8902  axdc4lem  8903  axcclem  8905  ac6num  8927  ac6c4  8929  iundom2g  8983  fpwwe2  9086  pwfseqlem1  9101  pwfseqlem4a  9104  pwfseqlem4  9105  ltapi  9346  ltmpi  9347  eluzadd  11211  fzsubel  11860  elfzp1b  11897  axdc4uzlem  12233  wrd2ind  12888  smuval  14534  prdsbasprj  15448  xpsfrnel  15547  ismri2dad  15621  mreexd  15626  mreacs  15642  iscat  15656  iscatd  15657  iscatd2  15665  catcocl  15669  catpropd  15692  brssc  15797  issubc  15818  subcidcl  15827  subccocl  15828  isfunc  15847  isfuncd  15848  cofucl  15871  funcres2b  15880  fuciso  15958  yonedalem3  16243  yonffthlem  16245  ismgm  16567  ismndOLD  16620  ismndd  16637  eqgfval  16943  efgsdm  17458  efgsdmi  17460  efgsrel  17462  efgsp1  17465  efgsres  17466  dprdwdOLD  17722  dprdfcl  17724  ablfaclem3  17798  isdrngd  18078  issrng  18156  issrngd  18167  islmodd  18175  islbs  18377  lbsind  18381  lbspropd  18400  islbs2  18455  lbsextlem4  18462  lbsextg  18463  zndvds  19197  isphl  19272  isphld  19298  phlpropd  19299  frlmlbs  19432  islindf  19447  islinds2  19448  lindfind  19451  lindsind  19452  lindsind2  19454  lindfrn  19456  lindfmm  19462  lsslindf  19465  mat1dimmul  19578  istps  20028  tpspropd  20032  eltpsg  20037  islp  20233  1stcelcls  20553  kgeni  20629  kgencn2  20649  ptpjpre1  20663  elptr2  20666  ptbasin  20669  ptbasfi  20673  ptpjcn  20703  ptpjopn  20704  ptcld  20705  ptcldmpt  20706  ptclsg  20707  ptcnp  20714  qtopval  20787  ptcmplem2  21146  ptcmplem3  21147  ptcmplem4  21148  istmd  21167  istgp  21170  tmdgsum  21188  istlm  21277  isusp  21354  prdsdsf  21460  prdsxmet  21462  isms  21542  mspropd  21567  setsxms  21572  setsms  21573  tmsxms  21579  tmsms  21580  isnrg  21741  tngnrg  21755  bcthlem2  22371  bcthlem3  22372  bcthlem4  22373  bcthlem5  22374  iscms  22391  cmspropd  22395  cmsss  22396  shft2rab  22539  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  vitalilem2  22646  vitalilem3  22647  vitali  22650  limcfval  22906  limcmpt2  22918  limcres  22920  cnplimc  22921  cnlimci  22923  elcpn  22967  uc1pval  23169  ig1pcl  23206  ig1pclOLD  23212  jensen  23993  axtgcont  24596  tglngval  24675  ishlg  24726  mirbtwnb  24796  islnopp  24860  outpasch  24876  colhp  24891  trgcopy  24925  trgcopyeu  24927  dfcgra2  24950  acopyeu  24954  isinag  24958  tgasa1  24968  nbgraop  25230  nbgraopALT  25231  imsmet  26404  smcn  26415  iscbn  26587  sbceqbidf  28196  isslmd  28592  submateq  28709  lmatcl  28716  ispcmp  28758  zhmnrg  28845  ismntoplly  28903  inelpisys  29050  sigapildsys  29058  fiunelcarsg  29221  eulerpartlemgvv  29282  eulerpart  29288  ptpcon  30028  cvmscbv  30053  cvmshmeo  30066  cvmsss2  30069  cvmliftlem7  30086  cvmliftlem10  30089  cvmlift2lem11  30108  cvmlift2lem12  30109  elmpps  30283  ghomgrplem  30379  csbfinxpg  31850  ptrest  32003  upixp  32120  sdclem1  32136  sstotbnd2  32170  prdsbnd2  32191  isprrngo  32347  isopos  32817  isatl  32936  isnacs3  35623  nacsfix  35625  mzpclall  35640  dnnumch1  35973  dnwech  35977  aomclem3  35985  aomclem8  35990  dfac11  35991  islmodfg  35998  sblpnf  36728  rusbcALT  36860  sbcel12gOLD  36975  choicefi  37552  climsuselem1  37783  climsuse  37784  cncfuni  37861  dvnprodlem1  37918  stoweidlem31  38004  stoweidlem59  38032  fourierdlem46  38128  fourierdlem62  38144  fourierdlem72  38154  fourierdlem79  38161  fourierdlem88  38170  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  fourierdlem112  38194  qndenserrnbllem  38275  issal  38287  sge0tsms  38336  sge0iunmpt  38374  sge0seq  38402  ovnsubaddlem1  38510  ovnsubaddlem2  38511  hoidmvlelem3  38537  hoidmvlelem4  38538  rrnmbl  38554  hoiqssbllem3  38564  hspmbl  38569  hoimbl  38571  dfateq12d  38776  1wlkp1lem3  39871  ismgmd  40284  iscllaw  40333  islininds  40747
  Copyright terms: Public domain W3C validator