Theorem eleq12i 2856

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 2855	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷)
3		eleq1i.1	. . 3 ⊢ 𝐴 = 𝐵
4	3	eleq1i 2854	. 2 ⊢ (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷)
5	2, 4	bitri 278	1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2146

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

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

This theorem is used by:  sbcel12  4371  smndex1n0mnd  19123  zclmncvs  25481  gausslemma2dlem4  27708  bnj98  35550  j00smo  35959  elmpst  36422  elmpps  36459  sbceqbii  37107  cbvsbcvw2  37146  oaordnrex  44437  omnord1ex  44446  oenord1ex  44457  wfaxpow  46126  unirnmapsn  46366  gpgprismgr4cycllem8  49339  isprmrng  49572