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  4664  elvvuni  4782  elrnmpt1  4974  canth  5951  smoeq  6434  smores  6436  smores2  6438  iordsmo  6441  nnaordi  6652  nnaordr  6654  fvixp  6848  cbvixp  6860  mptelixpg  6879  opabfi  7096  exmidaclem  7386  cc1  7447  cc2lem  7448  cc3  7450  ltapig  7521  ltmpig  7522  fzsubel  10252  elfzp1b  10289  wrd2ind  11250  ennnfonelemg  12969  ennnfonelemp1  12972  ennnfonelemnn0  12988  ctiunctlemu1st  13000  ctiunctlemu2nd  13001  ctiunctlemudc  13003  ctiunctlemfo  13005  prdsbasprj  13310  xpsfrnel  13372  ismgm  13385  mgm1  13398  issgrpd  13440  ismndd  13465  eqgfval  13754  ringcl  13971  unitinvcl  14081  aprval  14240  aprap  14244  islmodd  14251  rspcl  14449  rnglidlmmgm  14454  zndvds  14607  istps  14700  tpspropd  14704  eltpsg  14708  isms  15121  mspropd  15146  cnlimci  15341