Theorem eleq12d 2267

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 2266	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2265	. 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 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

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

This theorem is referenced by:  cbvraldva2  2736  cbvrexdva2  2737  cdeqel  2985  ru  2988  sbceqbid  2996  sbcel12g  3099  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  onintexmid  4610  elvvuni  4728  elrnmpt1  4918  canth  5878  smoeq  6357  smores  6359  smores2  6361  iordsmo  6364  nnaordi  6575  nnaordr  6577  fvixp  6771  cbvixp  6783  mptelixpg  6802  opabfi  7008  exmidaclem  7293  cc1  7350  cc2lem  7351  cc3  7353  ltapig  7424  ltmpig  7425  fzsubel  10154  elfzp1b  10191  ennnfonelemg  12647  ennnfonelemp1  12650  ennnfonelemnn0  12666  ctiunctlemu1st  12678  ctiunctlemu2nd  12679  ctiunctlemudc  12681  ctiunctlemfo  12683  prdsbasprj  12986  xpsfrnel  13048  ismgm  13061  mgm1  13074  issgrpd  13116  ismndd  13141  eqgfval  13430  ringcl  13647  unitinvcl  13757  aprval  13916  aprap  13920  islmodd  13927  rspcl  14125  rnglidlmmgm  14130  zndvds  14283  istps  14376  tpspropd  14380  eltpsg  14384  isms  14797  mspropd  14822  cnlimci  15017