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 ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   e. wcel 2209

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587  ax-ext 2220

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

This theorem is referenced by:  cbvraldva2  2793  cbvrexdva2  2794  cdeqel  3047  ru  3050  sbceqbid  3058  sbcel12g  3162  cbvralcsf  3210  cbvrexcsf  3211  cbvreucsf  3212  cbvrabcsf  3213  onintexmid  4715  elvvuni  4834  elrnmpt1  5028  canth  6026  smoeq  6551  smores  6553  smores2  6555  iordsmo  6558  nnaordi  6771  nnaordr  6773  fvixp  6975  cbvixp  6987  mptelixpg  7006  opabfi  7237  exmidaclem  7554  cc1  7621  cc2lem  7622  cc3  7624  ltapig  7695  ltmpig  7696  fzsubel  10444  elfzp1b  10482  wrd2ind  11473  ennnfonelemg  13272  ennnfonelemp1  13275  ennnfonelemnn0  13291  ctiunctlemu1st  13303  ctiunctlemu2nd  13304  ctiunctlemudc  13306  ctiunctlemfo  13308  xpsfrnel  13642  ismgm  13654  mgm1  13667  issgrpd  13704  ismndd  13727  eqgfval  14002  prdsbasprj  14159  ringcl  14291  unitinvcl  14403  aprval  14564  aprap  14571  aprprop  14574  islmodd  14602  rspcl  14800  rnglidlmmgm  14805  zndvds  14956  istps  15056  tpspropd  15060  eltpsg  15064  isms  15477  mspropd  15502  cnlimci  15697  depindlem2  16662