Theorem eleq12d 2305

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 2304	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2303	. 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 1398   e. wcel 2205

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2216

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

This theorem is referenced by:  cbvraldva2  2787  cbvrexdva2  2788  cdeqel  3041  ru  3044  sbceqbid  3052  sbcel12g  3156  cbvralcsf  3204  cbvrexcsf  3205  cbvreucsf  3206  cbvrabcsf  3207  onintexmid  4700  elvvuni  4819  elrnmpt1  5013  canth  6009  smoeq  6534  smores  6536  smores2  6538  iordsmo  6541  nnaordi  6754  nnaordr  6756  fvixp  6951  cbvixp  6963  mptelixpg  6982  opabfi  7213  exmidaclem  7528  cc1  7595  cc2lem  7596  cc3  7598  ltapig  7669  ltmpig  7670  fzsubel  10415  elfzp1b  10453  wrd2ind  11440  ennnfonelemg  13238  ennnfonelemp1  13241  ennnfonelemnn0  13257  ctiunctlemu1st  13269  ctiunctlemu2nd  13270  ctiunctlemudc  13272  ctiunctlemfo  13274  xpsfrnel  13608  ismgm  13620  mgm1  13633  issgrpd  13675  ismndd  13698  eqgfval  13975  prdsbasprj  14124  ringcl  14256  unitinvcl  14368  aprval  14529  aprap  14536  aprprop  14539  islmodd  14567  rspcl  14765  rnglidlmmgm  14770  zndvds  14923  istps  15023  tpspropd  15027  eltpsg  15031  isms  15444  mspropd  15469  cnlimci  15664  depindlem2  16628