Theorem eleq12d 2302

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

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 2213

This theorem depends on definitions:  df-bi 117  df-cleq 2224  df-clel 2227

This theorem is referenced by:  cbvraldva2  2775  cbvrexdva2  2776  cdeqel  3028  ru  3031  sbceqbid  3039  sbcel12g  3143  cbvralcsf  3191  cbvrexcsf  3192  cbvreucsf  3193  cbvrabcsf  3194  onintexmid  4677  elvvuni  4796  elrnmpt1  4989  canth  5979  smoeq  6499  smores  6501  smores2  6503  iordsmo  6506  nnaordi  6719  nnaordr  6721  fvixp  6915  cbvixp  6927  mptelixpg  6946  opabfi  7175  exmidaclem  7466  cc1  7527  cc2lem  7528  cc3  7530  ltapig  7601  ltmpig  7602  fzsubel  10340  elfzp1b  10377  wrd2ind  11353  ennnfonelemg  13087  ennnfonelemp1  13090  ennnfonelemnn0  13106  ctiunctlemu1st  13118  ctiunctlemu2nd  13119  ctiunctlemudc  13121  ctiunctlemfo  13123  prdsbasprj  13428  xpsfrnel  13490  ismgm  13503  mgm1  13516  issgrpd  13558  ismndd  13583  eqgfval  13872  ringcl  14090  unitinvcl  14201  aprval  14361  aprap  14365  islmodd  14372  rspcl  14570  rnglidlmmgm  14575  zndvds  14728  istps  14826  tpspropd  14830  eltpsg  14834  isms  15247  mspropd  15272  cnlimci  15467  depindlem2  16431