Theorem eleq12d 2278

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 2277	. 2 |- ( ph -> ( A e. C <-> A e. D ) )
3		eleq1d.1	. . 3 |- ( ph -> A = B )
4	3	eleq1d 2276	. 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 2178

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-clel 2203

This theorem is referenced by:  cbvraldva2  2749  cbvrexdva2  2750  cdeqel  3001  ru  3004  sbceqbid  3012  sbcel12g  3116  cbvralcsf  3164  cbvrexcsf  3165  cbvreucsf  3166  cbvrabcsf  3167  onintexmid  4639  elvvuni  4757  elrnmpt1  4948  canth  5920  smoeq  6399  smores  6401  smores2  6403  iordsmo  6406  nnaordi  6617  nnaordr  6619  fvixp  6813  cbvixp  6825  mptelixpg  6844  opabfi  7061  exmidaclem  7351  cc1  7412  cc2lem  7413  cc3  7415  ltapig  7486  ltmpig  7487  fzsubel  10217  elfzp1b  10254  wrd2ind  11214  ennnfonelemg  12889  ennnfonelemp1  12892  ennnfonelemnn0  12908  ctiunctlemu1st  12920  ctiunctlemu2nd  12921  ctiunctlemudc  12923  ctiunctlemfo  12925  prdsbasprj  13229  xpsfrnel  13291  ismgm  13304  mgm1  13317  issgrpd  13359  ismndd  13384  eqgfval  13673  ringcl  13890  unitinvcl  14000  aprval  14159  aprap  14163  islmodd  14170  rspcl  14368  rnglidlmmgm  14373  zndvds  14526  istps  14619  tpspropd  14623  eltpsg  14627  isms  15040  mspropd  15065  cnlimci  15260