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  10466  elfzp1b  10504  wrd2ind  11495  ennnfonelemg  13294  ennnfonelemp1  13297  ennnfonelemnn0  13313  ctiunctlemu1st  13325  ctiunctlemu2nd  13326  ctiunctlemudc  13328  ctiunctlemfo  13330  xpsfrnel  13665  ismgm  13677  mgm1  13690  issgrpd  13727  ismndd  13750  eqgfval  14025  prdsbasprj  14182  ringcl  14317  unitinvcl  14430  aprval  14591  aprap  14598  aprprop  14601  islmodd  14629  rspcl  14828  rnglidlmmgm  14833  zndvds  14984  istps  15133  tpspropd  15137  eltpsg  15141  isms  15554  mspropd  15579  cnlimci  15774  depindlem2  16748