Theorem eleq12d 2210

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 2209	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2208	. 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 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135

This theorem is referenced by:  cbvraldva2  2661  cbvrexdva2  2662  cdeqel  2905  ru  2908  sbcel12g  3017  cbvralcsf  3062  cbvrexcsf  3063  cbvreucsf  3064  cbvrabcsf  3065  onintexmid  4487  elvvuni  4603  elrnmpt1  4790  smoeq  6187  smores  6189  smores2  6191  iordsmo  6194  nnaordi  6404  nnaordr  6406  fvixp  6597  cbvixp  6609  mptelixpg  6628  exmidaclem  7064  ltapig  7146  ltmpig  7147  fzsubel  9840  elfzp1b  9877  ennnfonelemg  11916  ennnfonelemp1  11919  ennnfonelemnn0  11935  ctiunctlemu1st  11947  ctiunctlemu2nd  11948  ctiunctlemudc  11950  ctiunctlemfo  11952  istps  12199  tpspropd  12203  eltpsg  12207  isms  12622  mspropd  12647  cnlimci  12811