Theorem eleq12d 2303

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 2302	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2301	. 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 1398   e. wcel 2203

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-cleq 2225  df-clel 2228

This theorem is referenced by:  cbvraldva2  2785  cbvrexdva2  2786  cdeqel  3038  ru  3041  sbceqbid  3049  sbcel12g  3153  cbvralcsf  3201  cbvrexcsf  3202  cbvreucsf  3203  cbvrabcsf  3204  onintexmid  4695  elvvuni  4814  elrnmpt1  5008  canth  6001  smoeq  6521  smores  6523  smores2  6525  iordsmo  6528  nnaordi  6741  nnaordr  6743  fvixp  6938  cbvixp  6950  mptelixpg  6969  opabfi  7200  exmidaclem  7515  cc1  7579  cc2lem  7580  cc3  7582  ltapig  7653  ltmpig  7654  fzsubel  10394  elfzp1b  10431  wrd2ind  11415  ennnfonelemg  13154  ennnfonelemp1  13157  ennnfonelemnn0  13173  ctiunctlemu1st  13185  ctiunctlemu2nd  13186  ctiunctlemudc  13188  ctiunctlemfo  13190  prdsbasprj  13495  xpsfrnel  13557  ismgm  13570  mgm1  13583  issgrpd  13625  ismndd  13650  eqgfval  13939  ringcl  14157  unitinvcl  14268  aprval  14428  aprap  14432  islmodd  14441  rspcl  14639  rnglidlmmgm  14644  zndvds  14797  istps  14897  tpspropd  14901  eltpsg  14905  isms  15318  mspropd  15343  cnlimci  15538  depindlem2  16502