Theorem eleq12i 1962

Description: Inference from equality to equivalence of membership.

Hypotheses

Ref	Expression
eleq1i.1	|- A = B
eleq12i.2	|- C = D

Assertion

Ref	Expression
eleq12i	|- (A e. C <-> B e. D)

Proof of Theorem eleq12i

Step	Hyp	Ref	Expression
1		eleq12i.2	. . 3 |- C = D
2	1	eleq2i 1961	. 2 |- (A e. C <-> A e. D)
3		eleq1i.1	. . 3 |- A = B
4	3	eleq1i 1960	. 2 |- (A e. D <-> B e. D)
5	2, 4	bitri 190	1 |- (A e. C <-> B e. D)

Syntax hints:   <-> wb 163   = wceq 1298   e. wcel 1300

This theorem is referenced by:  sbcel12g 2552  sbcel12gOLD 2553  1q 6209  0r 6341  1r 6342  m1r 6343  fsumshft 8291  bnj98 13221  eucalg 13755  repcpwti 14503  geme2 14617  txcnoprab 15911  ispgrag 16301

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-cleq 1877  df-clel 1880

Copyright terms: Public domain