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  3024  ru  3027  sbceqbid  3035  sbcel12g  3139  cbvralcsf  3187  cbvrexcsf  3188  cbvreucsf  3189  cbvrabcsf  3190  onintexmid  4665  elvvuni  4783  elrnmpt1  4975  canth  5958  smoeq  6442  smores  6444  smores2  6446  iordsmo  6449  nnaordi  6662  nnaordr  6664  fvixp  6858  cbvixp  6870  mptelixpg  6889  opabfi  7111  exmidaclem  7401  cc1  7462  cc2lem  7463  cc3  7465  ltapig  7536  ltmpig  7537  fzsubel  10268  elfzp1b  10305  wrd2ind  11270  ennnfonelemg  12989  ennnfonelemp1  12992  ennnfonelemnn0  13008  ctiunctlemu1st  13020  ctiunctlemu2nd  13021  ctiunctlemudc  13023  ctiunctlemfo  13025  prdsbasprj  13330  xpsfrnel  13392  ismgm  13405  mgm1  13418  issgrpd  13460  ismndd  13485  eqgfval  13774  ringcl  13991  unitinvcl  14102  aprval  14261  aprap  14265  islmodd  14272  rspcl  14470  rnglidlmmgm  14475  zndvds  14628  istps  14721  tpspropd  14725  eltpsg  14729  isms  15142  mspropd  15167  cnlimci  15362