Theorem eleq12d 2248

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 2247	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2246	. 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 1353   e. wcel 2148

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-clel 2173

This theorem is referenced by:  cbvraldva2  2710  cbvrexdva2  2711  cdeqel  2958  ru  2961  sbceqbid  2969  sbcel12g  3072  cbvralcsf  3119  cbvrexcsf  3120  cbvreucsf  3121  cbvrabcsf  3122  onintexmid  4572  elvvuni  4690  elrnmpt1  4878  canth  5828  smoeq  6290  smores  6292  smores2  6294  iordsmo  6297  nnaordi  6508  nnaordr  6510  fvixp  6702  cbvixp  6714  mptelixpg  6733  exmidaclem  7206  cc1  7263  cc2lem  7264  cc3  7266  ltapig  7336  ltmpig  7337  fzsubel  10057  elfzp1b  10094  ennnfonelemg  12398  ennnfonelemp1  12401  ennnfonelemnn0  12417  ctiunctlemu1st  12429  ctiunctlemu2nd  12430  ctiunctlemudc  12432  ctiunctlemfo  12434  ismgm  12730  mgm1  12743  ismndd  12792  eqgfval  13034  ringcl  13149  unitinvcl  13245  aprval  13293  aprap  13297  istps  13423  tpspropd  13427  eltpsg  13431  isms  13846  mspropd  13871  cnlimci  14035