Theorem eleq12d 2275

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 2274	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2273	. 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 1372   e. wcel 2175

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-cleq 2197  df-clel 2200

This theorem is referenced by:  cbvraldva2  2744  cbvrexdva2  2745  cdeqel  2993  ru  2996  sbceqbid  3004  sbcel12g  3107  cbvralcsf  3155  cbvrexcsf  3156  cbvreucsf  3157  cbvrabcsf  3158  onintexmid  4620  elvvuni  4738  elrnmpt1  4928  canth  5896  smoeq  6375  smores  6377  smores2  6379  iordsmo  6382  nnaordi  6593  nnaordr  6595  fvixp  6789  cbvixp  6801  mptelixpg  6820  opabfi  7034  exmidaclem  7319  cc1  7376  cc2lem  7377  cc3  7379  ltapig  7450  ltmpig  7451  fzsubel  10181  elfzp1b  10218  ennnfonelemg  12745  ennnfonelemp1  12748  ennnfonelemnn0  12764  ctiunctlemu1st  12776  ctiunctlemu2nd  12777  ctiunctlemudc  12779  ctiunctlemfo  12781  prdsbasprj  13085  xpsfrnel  13147  ismgm  13160  mgm1  13173  issgrpd  13215  ismndd  13240  eqgfval  13529  ringcl  13746  unitinvcl  13856  aprval  14015  aprap  14019  islmodd  14026  rspcl  14224  rnglidlmmgm  14229  zndvds  14382  istps  14475  tpspropd  14479  eltpsg  14483  isms  14896  mspropd  14921  cnlimci  15116