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  4667  elvvuni  4786  elrnmpt1  4979  canth  5962  smoeq  6449  smores  6451  smores2  6453  iordsmo  6456  nnaordi  6669  nnaordr  6671  fvixp  6865  cbvixp  6877  mptelixpg  6896  opabfi  7121  exmidaclem  7411  cc1  7472  cc2lem  7473  cc3  7475  ltapig  7546  ltmpig  7547  fzsubel  10283  elfzp1b  10320  wrd2ind  11291  ennnfonelemg  13011  ennnfonelemp1  13014  ennnfonelemnn0  13030  ctiunctlemu1st  13042  ctiunctlemu2nd  13043  ctiunctlemudc  13045  ctiunctlemfo  13047  prdsbasprj  13352  xpsfrnel  13414  ismgm  13427  mgm1  13440  issgrpd  13482  ismndd  13507  eqgfval  13796  ringcl  14013  unitinvcl  14124  aprval  14283  aprap  14287  islmodd  14294  rspcl  14492  rnglidlmmgm  14497  zndvds  14650  istps  14743  tpspropd  14747  eltpsg  14751  isms  15164  mspropd  15189  cnlimci  15384