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 1397   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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-ext 2213

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

This theorem is referenced by:  cbvraldva2  2774  cbvrexdva2  2775  cdeqel  3027  ru  3030  sbceqbid  3038  sbcel12g  3142  cbvralcsf  3190  cbvrexcsf  3191  cbvreucsf  3192  cbvrabcsf  3193  onintexmid  4671  elvvuni  4790  elrnmpt1  4983  canth  5969  smoeq  6456  smores  6458  smores2  6460  iordsmo  6463  nnaordi  6676  nnaordr  6678  fvixp  6872  cbvixp  6884  mptelixpg  6903  opabfi  7132  exmidaclem  7423  cc1  7484  cc2lem  7485  cc3  7487  ltapig  7558  ltmpig  7559  fzsubel  10295  elfzp1b  10332  wrd2ind  11308  ennnfonelemg  13042  ennnfonelemp1  13045  ennnfonelemnn0  13061  ctiunctlemu1st  13073  ctiunctlemu2nd  13074  ctiunctlemudc  13076  ctiunctlemfo  13078  prdsbasprj  13383  xpsfrnel  13445  ismgm  13458  mgm1  13471  issgrpd  13513  ismndd  13538  eqgfval  13827  ringcl  14045  unitinvcl  14156  aprval  14315  aprap  14319  islmodd  14326  rspcl  14524  rnglidlmmgm  14529  zndvds  14682  istps  14775  tpspropd  14779  eltpsg  14783  isms  15196  mspropd  15221  cnlimci  15416  depindlem2  16377