Theorem eleq12d 2158

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

Syntax hints:   -> wi 4   <-> wb 103   = wceq 1289   e. wcel 1438

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084

This theorem is referenced by:  cbvraldva2  2594  cbvrexdva2  2595  cdeqel  2836  ru  2839  sbcel12g  2946  cbvralcsf  2990  cbvrexcsf  2991  cbvreucsf  2992  cbvrabcsf  2993  onintexmid  4386  elvvuni  4498  elrnmpt1  4682  smoeq  6047  smores  6049  smores2  6051  iordsmo  6054  nnaordi  6257  nnaordr  6259  ltapig  6887  ltmpig  6888  fzsubel  9463  elfzp1b  9499