Theorem eleq12i 2857

Description: Inference from equality to equivalence of membership. (Contributed by NM, 31-May-1994.)

Hypotheses

Ref	Expression
eleq1i.1	⊢ 𝐴 = 𝐵
eleq12i.2	⊢ 𝐶 = 𝐷

Assertion

Ref	Expression
eleq12i	⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)

Proof of Theorem eleq12i

Step	Hyp	Ref	Expression
1		eleq12i.2	. . 3 ⊢ 𝐶 = 𝐷
2	1	eleq2i 2856	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)
3		eleq1i.1	. . 3 ⊢ 𝐴 = 𝐵
4	3	eleq1i 2855	. 2 ⊢ (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷)
5	2, 4	bitri 278	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-clel 2839

This theorem is used by:  sbcel12  4372  smndex1n0mnd  19161  zclmncvs  25524  gausslemma2dlem4  27753  bnj98  35608  j00smo  36046  elmpst  36509  elmpps  36546  sbceqbii  37195  cbvsbcvw2  37234  oaordnrex  44558  omnord1ex  44567  oenord1ex  44578  wfaxpow  46251  unirnmapsn  46500  gpgprismgr4cycllem8  49473  isprmrng  49764