Theorem eleq12d 2276

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201

This theorem is referenced by:  cbvraldva2  2745  cbvrexdva2  2746  cdeqel  2994  ru  2997  sbceqbid  3005  sbcel12g  3108  cbvralcsf  3156  cbvrexcsf  3157  cbvreucsf  3158  cbvrabcsf  3159  onintexmid  4621  elvvuni  4739  elrnmpt1  4929  canth  5897  smoeq  6376  smores  6378  smores2  6380  iordsmo  6383  nnaordi  6594  nnaordr  6596  fvixp  6790  cbvixp  6802  mptelixpg  6821  opabfi  7035  exmidaclem  7320  cc1  7377  cc2lem  7378  cc3  7380  ltapig  7451  ltmpig  7452  fzsubel  10182  elfzp1b  10219  ennnfonelemg  12774  ennnfonelemp1  12777  ennnfonelemnn0  12793  ctiunctlemu1st  12805  ctiunctlemu2nd  12806  ctiunctlemudc  12808  ctiunctlemfo  12810  prdsbasprj  13114  xpsfrnel  13176  ismgm  13189  mgm1  13202  issgrpd  13244  ismndd  13269  eqgfval  13558  ringcl  13775  unitinvcl  13885  aprval  14044  aprap  14048  islmodd  14055  rspcl  14253  rnglidlmmgm  14258  zndvds  14411  istps  14504  tpspropd  14508  eltpsg  14512  isms  14925  mspropd  14950  cnlimci  15145