Theorem eleq12d 2264

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 2263	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2262	. 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 2164

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545  ax-ext 2175

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

This theorem is referenced by:  cbvraldva2  2733  cbvrexdva2  2734  cdeqel  2981  ru  2984  sbceqbid  2992  sbcel12g  3095  cbvralcsf  3143  cbvrexcsf  3144  cbvreucsf  3145  cbvrabcsf  3146  onintexmid  4605  elvvuni  4723  elrnmpt1  4913  canth  5871  smoeq  6343  smores  6345  smores2  6347  iordsmo  6350  nnaordi  6561  nnaordr  6563  fvixp  6757  cbvixp  6769  mptelixpg  6788  opabfi  6992  exmidaclem  7268  cc1  7325  cc2lem  7326  cc3  7328  ltapig  7398  ltmpig  7399  fzsubel  10126  elfzp1b  10163  ennnfonelemg  12560  ennnfonelemp1  12563  ennnfonelemnn0  12579  ctiunctlemu1st  12591  ctiunctlemu2nd  12592  ctiunctlemudc  12594  ctiunctlemfo  12596  xpsfrnel  12927  ismgm  12940  mgm1  12953  issgrpd  12995  ismndd  13018  eqgfval  13292  ringcl  13509  unitinvcl  13619  aprval  13778  aprap  13782  islmodd  13789  rspcl  13987  rnglidlmmgm  13992  zndvds  14137  istps  14200  tpspropd  14204  eltpsg  14208  isms  14621  mspropd  14646  cnlimci  14827