Theorem eleq12d 2302

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 2301	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2300	. 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 1397   e. wcel 2202

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  cbvraldva2  2774  cbvrexdva2  2775  cdeqel  3027  ru  3030  sbceqbid  3038  sbcel12g  3142  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  onintexmid  4671  elvvuni  4790  elrnmpt1  4983  canth  5968  smoeq  6455  smores  6457  smores2  6459  iordsmo  6462  nnaordi  6675  nnaordr  6677  fvixp  6871  cbvixp  6883  mptelixpg  6902  opabfi  7131  exmidaclem  7422  cc1  7483  cc2lem  7484  cc3  7486  ltapig  7557  ltmpig  7558  fzsubel  10294  elfzp1b  10331  wrd2ind  11303  ennnfonelemg  13023  ennnfonelemp1  13026  ennnfonelemnn0  13042  ctiunctlemu1st  13054  ctiunctlemu2nd  13055  ctiunctlemudc  13057  ctiunctlemfo  13059  prdsbasprj  13364  xpsfrnel  13426  ismgm  13439  mgm1  13452  issgrpd  13494  ismndd  13519  eqgfval  13808  ringcl  14025  unitinvcl  14136  aprval  14295  aprap  14299  islmodd  14306  rspcl  14504  rnglidlmmgm  14509  zndvds  14662  istps  14755  tpspropd  14759  eltpsg  14763  isms  15176  mspropd  15201  cnlimci  15396