Theorem eleq2d 2420

Description: Deduction from equality to equivalence of membership. (Contributed by NM, 27-Dec-1993.)

Hypothesis

Ref	Expression
eleq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
eleq2d	⊢ (φ → (C ∈ A ↔ C ∈ B))

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (φ → A = B)
2		eleq2 2414	. 2 ⊢ (A = B → (C ∈ A ↔ C ∈ B))
3	1, 2	syl 15	1 ⊢ (φ → (C ∈ A ↔ C ∈ B))

Syntax hints:   → wi 4   ↔ wb 176   = wceq 1642   ∈ wcel 1710

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-cleq 2346  df-clel 2349

This theorem is referenced by:  eleq12d  2421  eleqtrd  2429  neleqtrd  2448  neleqtrrd  2449  abeq2d  2462  nfceqdf  2488  drnfc1  2505  drnfc2  2506  sbcbid  3099  cbvcsb  3140  sbcel1g  3155  csbeq2d  3160  csbie2g  3182  cbvralcsf  3198  cbvreucsf  3200  cbvrabcsf  3201  cbviun  4003  cbviin  4004  iinxsng  4042  iinxprg  4043  iunxsng  4044  nnsucelr  4428  nnadjoin  4520  tfinnn  4534  opeliunxp  4820  opeliunxp2  4822  iunxpf  4829  funfni  5183  fun11iun  5305  fvelrnb  5365  fniniseg  5371  fvun1  5379  eqfnfv  5392  elpreima  5407  dff3  5420  dffo4  5423  eluniima  5469  dff13  5471  isoini  5497  ovelrn  5608  mpteq12f  5655  mpt2eq123dv  5663  cbvmpt2x  5678  ovmpt2x  5712  fmpt2x  5730  clos1basesucg  5884  erref  5959  ereldm  5971  elmapg  6012  elpmg  6013  enpw1  6062  enprmaplem3  6078  nenpw1pwlem2  6085  elce  6175  nmembers1  6271