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  2711  cbvrexdva2  2712  cdeqel  2959  ru  2962  sbceqbid  2970  sbcel12g  3073  cbvralcsf  3120  cbvrexcsf  3121  cbvreucsf  3122  cbvrabcsf  3123  onintexmid  4573  elvvuni  4691  elrnmpt1  4879  canth  5829  smoeq  6291  smores  6293  smores2  6295  iordsmo  6298  nnaordi  6509  nnaordr  6511  fvixp  6703  cbvixp  6715  mptelixpg  6734  exmidaclem  7207  cc1  7264  cc2lem  7265  cc3  7267  ltapig  7337  ltmpig  7338  fzsubel  10060  elfzp1b  10097  ennnfonelemg  12404  ennnfonelemp1  12407  ennnfonelemnn0  12423  ctiunctlemu1st  12435  ctiunctlemu2nd  12436  ctiunctlemudc  12438  ctiunctlemfo  12440  xpsfrnel  12763  ismgm  12776  mgm1  12789  ismndd  12838  eqgfval  13081  ringcl  13196  unitinvcl  13292  aprval  13372  aprap  13376  islmodd  13383  istps  13535  tpspropd  13539  eltpsg  13543  isms  13956  mspropd  13981  cnlimci  14145