Theorem eleq12d 2267

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 2266	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2265	. 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 1364   e. wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  cbvraldva2  2736  cbvrexdva2  2737  cdeqel  2985  ru  2988  sbceqbid  2996  sbcel12g  3099  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  onintexmid  4609  elvvuni  4727  elrnmpt1  4917  canth  5875  smoeq  6348  smores  6350  smores2  6352  iordsmo  6355  nnaordi  6566  nnaordr  6568  fvixp  6762  cbvixp  6774  mptelixpg  6793  opabfi  6999  exmidaclem  7275  cc1  7332  cc2lem  7333  cc3  7335  ltapig  7405  ltmpig  7406  fzsubel  10135  elfzp1b  10172  ennnfonelemg  12620  ennnfonelemp1  12623  ennnfonelemnn0  12639  ctiunctlemu1st  12651  ctiunctlemu2nd  12652  ctiunctlemudc  12654  ctiunctlemfo  12656  xpsfrnel  12987  ismgm  13000  mgm1  13013  issgrpd  13055  ismndd  13078  eqgfval  13352  ringcl  13569  unitinvcl  13679  aprval  13838  aprap  13842  islmodd  13849  rspcl  14047  rnglidlmmgm  14052  zndvds  14205  istps  14268  tpspropd  14272  eltpsg  14276  isms  14689  mspropd  14714  cnlimci  14909