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  4722  elvvuni  4841  elrnmpt1  5035  canth  6039  smoeq  6565  smores  6567  smores2  6569  iordsmo  6572  nnaordi  6785  nnaordr  6787  fvixp  6989  cbvixp  7001  mptelixpg  7020  opabfi  7251  exmidaclem  7570  cc1  7637  cc2lem  7638  cc3  7640  ltapig  7711  ltmpig  7712  fzsubel  10483  elfzp1b  10521  wrd2ind  11517  ennnfonelemg  13352  ennnfonelemp1  13355  ennnfonelemnn0  13371  ctiunctlemu1st  13383  ctiunctlemu2nd  13384  ctiunctlemudc  13386  ctiunctlemfo  13388  xpsfrnel  13724  ismgm  13736  mgm1  13749  issgrpd  13786  ismndd  13809  eqgfval  14084  prdsbasprj  14289  ringcl  14424  unitinvcl  14539  aprval  14700  aprap  14707  aprprop  14710  islmodd  14738  rspcl  14937  rnglidlmmgm  14942  zndvds  15093  istps  15258  tpspropd  15262  eltpsg  15266  isms  15679  mspropd  15704  cnlimci  15899  depindlem2  16953