Theorem eleq12d 1585

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

Syntax hints:   -> wi 3   <-> wb 144   = wceq 992   e. wcel 994

This theorem is referenced by:  hbeld 1960  ru 1984  sucidg 3052  elvvuni 3315  canth 4205  tz7.49 4260  nnaordr 4376  omsmolem 4396  aceq3lem 4878  aceq5 4886  ac6lem 4900  numthlem 4929  unidom 4954  ltapi 5184  ltmpi 5185  fzsubel 6631  acdc3 7698  acdc2 7702  acdc5 7705  acdc 7707  cldval 7876  islp 7954  bcthlem16 8225  bcthlem17 8226  bcthlem18 8227  vacn 8588  nmcn 8593  isla 8929  shftefif1olem 9013  ghomgrplem 10674  osneisi 11018  isfil 11071  hartoglem 11435  isufil 11649  cbvixpv 11821  supclt 11854  eluzadd 11860  sdclem2 11876  sdc 11877  mettrifi2 11913  geomcau 11914  txcnoprab 11981  heiborlem30 12040

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain