Theorem eleq12d 2277

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

Hypotheses

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)
eleq12d.2	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
eleq12d	⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Proof of Theorem eleq12d

Step	Hyp	Ref	Expression
1		eleq12d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐷)
2	1	eleq2d 2276	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐴 ∈ 𝐷))
3		eleq1d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	eleq1d 2275	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐷 ↔ 𝐵 ∈ 𝐷))
5	2, 4	bitrd 188	1 ⊢ (𝜑 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1373   ∈ wcel 2177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199  df-clel 2202

This theorem is referenced by:  cbvraldva2  2746  cbvrexdva2  2747  cdeqel  2998  ru  3001  sbceqbid  3009  sbcel12g  3112  cbvralcsf  3160  cbvrexcsf  3161  cbvreucsf  3162  cbvrabcsf  3163  onintexmid  4628  elvvuni  4746  elrnmpt1  4937  canth  5909  smoeq  6388  smores  6390  smores2  6392  iordsmo  6395  nnaordi  6606  nnaordr  6608  fvixp  6802  cbvixp  6814  mptelixpg  6833  opabfi  7049  exmidaclem  7335  cc1  7392  cc2lem  7393  cc3  7395  ltapig  7466  ltmpig  7467  fzsubel  10197  elfzp1b  10234  wrd2ind  11194  ennnfonelemg  12844  ennnfonelemp1  12847  ennnfonelemnn0  12863  ctiunctlemu1st  12875  ctiunctlemu2nd  12876  ctiunctlemudc  12878  ctiunctlemfo  12880  prdsbasprj  13184  xpsfrnel  13246  ismgm  13259  mgm1  13272  issgrpd  13314  ismndd  13339  eqgfval  13628  ringcl  13845  unitinvcl  13955  aprval  14114  aprap  14118  islmodd  14125  rspcl  14323  rnglidlmmgm  14328  zndvds  14481  istps  14574  tpspropd  14578  eltpsg  14582  isms  14995  mspropd  15020  cnlimci  15215