Theorem eleq12d 2695

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

Step	Hyp	Ref	Expression
1		eleq12d.2	. . 3 |- ( ph -> C = D )
2	1	eleq2d 2687	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq12d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2686	. 2 |- ( ph -> ( A e. D <-> B e. D ) )
5	2, 4	bitrd 268	1 |- ( ph -> ( A e. C <-> B e. D ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  neleq12d  2901  cbvraldva2  3175  cbvrexdva2  3176  cdeqel  3431  ru  3434  sbceqbid  3442  cbvralcsf  3565  cbvreucsf  3567  cbvrabcsf  3568  sbcel12  3983  elvvuni  5179  elrnmpt1  5374  canth  6608  onnseq  7441  smoeq  7447  smores  7449  smores2  7451  iordsmo  7454  tz7.49  7540  nnaordr  7700  omsmolem  7733  fvixp  7913  cbvixp  7925  mptelixpg  7945  boxcutc  7951  ixpiunwdom  8496  elirr  8505  cantnflt  8569  oemapvali  8581  cantnflem1  8586  cantnf  8590  wemapwe  8594  cnfcom3lem  8600  infxpen  8837  dfac8alem  8852  dfac8clem  8855  ac5num  8859  acni2  8869  numacn  8872  acndom  8874  aceq3lem  8943  dfac5  8951  dfac9  8958  dfac13  8964  fin2i  9117  isfin2-2  9141  fin23lem27  9150  isfin3ds  9151  fin23lem17  9160  fin23lem39  9172  isf33lem  9188  isf34lem7  9201  isf34lem6  9202  fin1a2lem10  9231  fin1a2lem12  9233  hsmexlem4  9251  axcc2lem  9258  axcc3  9260  domtriomlem  9264  axdc2lem  9270  axdc3lem2  9273  axdc3lem3  9274  axdc3lem4  9275  axdc3  9276  axdc4lem  9277  axcclem  9279  ac6num  9301  ac6c4  9303  iundom2g  9362  fpwwe2  9465  pwfseqlem1  9480  pwfseqlem4a  9483  pwfseqlem4  9484  ltapi  9725  ltmpi  9726  eluzadd  11716  fzsubel  12377  elfzp1b  12417  axdc4uzlem  12782  wrd2ind  13477  smuval  15203  prdsbasprj  16132  xpsfrnel  16223  ismri2dad  16297  mreexd  16302  mreacs  16319  iscat  16333  iscatd  16334  iscatd2  16342  catcocl  16346  catpropd  16369  brssc  16474  issubc  16495  subcidcl  16504  subccocl  16505  isfunc  16524  isfuncd  16525  cofucl  16548  funcres2b  16557  fuciso  16635  yonedalem3  16920  yonffthlem  16922  ismgm  17243  issstrmgm  17252  ismndd  17313  eqgfval  17642  efgsdm  18143  efgsdmi  18145  efgsrel  18147  efgsp1  18150  efgsres  18151  dprdfcl  18412  ablfaclem3  18486  isdrngd  18772  issrng  18850  issrngd  18861  islmodd  18869  islbs  19076  lbsind  19080  lbspropd  19099  islbs2  19154  lbsextlem4  19161  lbsextg  19162  zndvds  19898  isphl  19973  isphld  19999  phlpropd  20000  frlmlbs  20136  islindf  20151  islinds2  20152  lindfind  20155  lindsind  20156  lindsind2  20158  lindfrn  20160  lindfmm  20166  lsslindf  20169  mat1dimmul  20282  istps  20738  tpspropd  20742  eltpsg  20747  islp  20944  1stcelcls  21264  kgeni  21340  kgencn2  21360  ptpjpre1  21374  elptr2  21377  ptbasin  21380  ptbasfi  21384  ptpjcn  21414  ptpjopn  21415  ptcld  21416  ptcldmpt  21417  ptclsg  21418  ptcnp  21425  qtopval  21498  ptcmplem2  21857  ptcmplem3  21858  ptcmplem4  21859  istmd  21878  istgp  21881  tmdgsum  21899  istlm  21988  isusp  22065  prdsdsf  22172  prdsxmet  22174  isms  22254  mspropd  22279  setsxms  22284  setsms  22285  tmsxms  22291  tmsms  22292  isnrg  22464  tngnrg  22478  bcthlem2  23122  bcthlem3  23123  bcthlem4  23124  bcthlem5  23125  iscms  23142  cmspropd  23146  cmsss  23147  shft2rab  23276  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  vitalilem2  23378  vitalilem3  23379  vitali  23382  limcfval  23636  limcmpt2  23648  limcres  23650  cnplimc  23651  cnlimci  23653  elcpn  23697  uc1pval  23899  ig1pcl  23935  jensen  24715  axtgcont  25368  tglngval  25446  ishlg  25497  mirbtwnb  25567  islnopp  25631  outpasch  25647  colhp  25662  trgcopy  25696  trgcopyeu  25698  dfcgra2  25721  acopyeu  25725  isinag  25729  tgasa1  25739  wlkp1lem3  26572  umgrwwlks2on  26850  imsmet  27546  smcn  27553  iscbn  27720  sbceqbidf  29321  isslmd  29755  submateq  29875  lmatcl  29882  ispcmp  29924  zhmnrg  30011  ismntoplly  30069  inelpisys  30217  sigapildsys  30225  fiunelcarsg  30378  eulerpartlemgvv  30438  eulerpart  30444  ptpconn  31215  cvmscbv  31240  cvmshmeo  31253  cvmsss2  31256  cvmliftlem7  31273  cvmliftlem10  31276  cvmlift2lem11  31295  cvmlift2lem12  31296  elmpps  31470  bj-ismoore  33059  csbfinxpg  33225  lindsenlbs  33404  ptrest  33408  upixp  33524  sdclem1  33539  sstotbnd2  33573  prdsbnd2  33594  isprrngo  33849  isopos  34467  isatl  34586  isnacs3  37273  nacsfix  37275  mzpclall  37290  dnnumch1  37614  dnwech  37618  aomclem3  37626  aomclem8  37631  dfac11  37632  islmodfg  37639  rfovcnvf1od  38298  sblpnf  38509  rusbcALT  38640  sbcel12gOLD  38754  choicefi  39392  climsuselem1  39839  climsuse  39840  cncfuni  40099  dvnprodlem1  40161  stoweidlem31  40248  stoweidlem59  40276  fourierdlem46  40369  fourierdlem62  40385  fourierdlem72  40395  fourierdlem79  40402  fourierdlem88  40411  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem112  40435  qndenserrnbllem  40514  ioorrnopnlem  40524  ioorrnopn  40525  ioorrnopnxr  40527  issal  40534  subsaliuncllem  40575  subsaliuncl  40576  subsalsal  40577  sge0tsms  40597  sge0iunmpt  40635  sge0seq  40663  ovnsubaddlem1  40784  ovnsubaddlem2  40785  hoidmvlelem3  40811  hoidmvlelem4  40812  rrnmbl  40828  hoiqssbllem3  40838  hspmbl  40843  hoimbl  40845  issmflem  40936  issmfd  40944  issmfdf  40946  smfpimltmpt  40955  issmfled  40966  smfpimltxrmpt  40967  smfmbfcex  40968  issmfgtd  40969  smflimlem1  40979  smflimlem2  40980  smflimlem3  40981  smflimlem6  40984  smfpimgtmpt  40989  smfpimgtxrmpt  40992  smfres  40997  smfco  41009  smfpimcclem  41013  smfpimcc  41014  dfateq12d  41209  ismgmd  41776  iscllaw  41825  islininds  42235