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  7565  cc1  7632  cc2lem  7633  cc3  7635  ltapig  7706  ltmpig  7707  fzsubel  10477  elfzp1b  10515  wrd2ind  11511  ennnfonelemg  13346  ennnfonelemp1  13349  ennnfonelemnn0  13365  ctiunctlemu1st  13377  ctiunctlemu2nd  13378  ctiunctlemudc  13380  ctiunctlemfo  13382  xpsfrnel  13718  ismgm  13730  mgm1  13743  issgrpd  13780  ismndd  13803  eqgfval  14078  prdsbasprj  14266  ringcl  14401  unitinvcl  14514  aprval  14675  aprap  14682  aprprop  14685  islmodd  14713  rspcl  14912  rnglidlmmgm  14917  zndvds  15068  istps  15224  tpspropd  15228  eltpsg  15232  isms  15645  mspropd  15670  cnlimci  15865  depindlem2  16914