Theorem eleq12d 1534

Description: Deduction from equality to equivalence of membership.

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 1533	. 2 |- (ph -> (A e. C <-> A e. D))
3		eleq1d.1	. . 3 |- (ph -> A = B)
4	3	eleq1d 1532	. 2 |- (ph -> (A e. D <-> B e. D))
5	2, 4	bitrd 526	1 |- (ph -> (A e. C <-> B e. D))

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953   e. wcel 955

This theorem is referenced by:  hbeld 1905  ru 1928  sucidg 3042  elvvuni 3219  canth 3892  tz7.49 3944  nnaordr 4220  omsmolem 4240  aceq3lem 4704  aceq5 4712  ac6lem 4726  numthlem 4755  unidom 4780  ltapi 5002  ltmpi 5003  fzsubelt 6433  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  cldval 7608  islp 7685  bcthlem16 7948  bcthlem17 7949  bcthlem18 7950  nmcn 8274  shftefif1olem 8661  shftefif1olemOLD 8662  ghomgrplem 10294  isfil 10433

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-cleq 1462  df-clel 1465

Copyright terms: Public domain