Theorem eleq12d 2300

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)

Hypotheses

Ref	Expression
eleq1d.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 2299	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2298	. 2 |- ( ph -> ( A e. D <-> B e. D ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( A e. C <-> B e. D ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1395   e. wcel 2200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  cbvraldva2  2772  cbvrexdva2  2773  cdeqel  3025  ru  3028  sbceqbid  3036  sbcel12g  3140  cbvralcsf  3188  cbvrexcsf  3189  cbvreucsf  3190  cbvrabcsf  3191  onintexmid  4669  elvvuni  4788  elrnmpt1  4981  canth  5964  smoeq  6451  smores  6453  smores2  6455  iordsmo  6458  nnaordi  6671  nnaordr  6673  fvixp  6867  cbvixp  6879  mptelixpg  6898  opabfi  7123  exmidaclem  7413  cc1  7474  cc2lem  7475  cc3  7477  ltapig  7548  ltmpig  7549  fzsubel  10285  elfzp1b  10322  wrd2ind  11294  ennnfonelemg  13014  ennnfonelemp1  13017  ennnfonelemnn0  13033  ctiunctlemu1st  13045  ctiunctlemu2nd  13046  ctiunctlemudc  13048  ctiunctlemfo  13050  prdsbasprj  13355  xpsfrnel  13417  ismgm  13430  mgm1  13443  issgrpd  13485  ismndd  13510  eqgfval  13799  ringcl  14016  unitinvcl  14127  aprval  14286  aprap  14290  islmodd  14297  rspcl  14495  rnglidlmmgm  14500  zndvds  14653  istps  14746  tpspropd  14750  eltpsg  14754  isms  15167  mspropd  15192  cnlimci  15387