Theorem eleq12d 2208

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 2207	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2206	. 2 |- ( ph -> ( A e. D <-> B e. D ) )
5	2, 4	bitrd 187	1 |- ( ph -> ( A e. C <-> B e. D ) )

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1331   e. wcel 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133

This theorem is referenced by:  cbvraldva2  2656  cbvrexdva2  2657  cdeqel  2900  ru  2903  sbcel12g  3012  cbvralcsf  3057  cbvrexcsf  3058  cbvreucsf  3059  cbvrabcsf  3060  onintexmid  4482  elvvuni  4598  elrnmpt1  4785  smoeq  6180  smores  6182  smores2  6184  iordsmo  6187  nnaordi  6397  nnaordr  6399  fvixp  6590  cbvixp  6602  mptelixpg  6621  exmidaclem  7057  ltapig  7139  ltmpig  7140  fzsubel  9833  elfzp1b  9870  ennnfonelemg  11905  ennnfonelemp1  11908  ennnfonelemnn0  11924  ctiunctlemu1st  11936  ctiunctlemu2nd  11937  ctiunctlemudc  11939  ctiunctlemfo  11941  istps  12188  tpspropd  12192  eltpsg  12196  isms  12611  mspropd  12636  cnlimci  12800