Theorem eleq12d 2309

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 2308	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2307	. 2 |- ( ph -> ( A e. D <-> B e. D ) )
5	2, 4	bitrd 188	1 |- ( ph -> ( A e. C <-> B e. D ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231  df-clel 2234

This theorem is used by:  cbvraldva2  2793  cbvrexdva2  2794  cdeqel  3047  ru  3050  sbceqbid  3058  sbcel12g  3162  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  onintexmid  4720  elvvuni  4839  elrnmpt1  5033  canth  6036  smoeq  6561  smores  6563  smores2  6565  iordsmo  6568  nnaordi  6781  nnaordr  6783  fvixp  6985  cbvixp  6997  mptelixpg  7016  opabfi  7247  exmidaclem  7564  cc1  7631  cc2lem  7632  cc3  7634  ltapig  7705  ltmpig  7706  fzsubel  10476  elfzp1b  10514  wrd2ind  11509  ennnfonelemg  13343  ennnfonelemp1  13346  ennnfonelemnn0  13362  ctiunctlemu1st  13374  ctiunctlemu2nd  13375  ctiunctlemudc  13377  ctiunctlemfo  13379  xpsfrnel  13714  ismgm  13726  mgm1  13739  issgrpd  13776  ismndd  13799  eqgfval  14074  prdsbasprj  14231  ringcl  14366  unitinvcl  14479  aprval  14640  aprap  14647  aprprop  14650  islmodd  14678  rspcl  14877  rnglidlmmgm  14882  zndvds  15033  istps  15182  tpspropd  15186  eltpsg  15190  isms  15603  mspropd  15628  cnlimci  15823  depindlem2  16846