Theorem eleq2d 2169

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

Hypothesis

Ref	Expression
eleq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

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

Proof of Theorem eleq2d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eleq2 2163	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1299   ∈ wcel 1448

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-4 1455  ax-17 1474  ax-ial 1482  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-cleq 2093  df-clel 2096

This theorem is referenced by:  eleq12d  2170  eleqtrd  2178  neleqtrd  2197  neleqtrrd  2198  abeq2d  2212  nfceqdf  2239  drnfc1  2257  drnfc2  2258  sbcbid  2918  cbvcsb  2959  sbcel1g  2972  csbeq2d  2977  csbie2g  3000  cbvralcsf  3012  cbvrexcsf  3013  cbvreucsf  3014  cbvrabcsf  3015  opeq1  3652  opeq2  3653  cbviun  3797  cbviin  3798  iinxsng  3833  iinxprg  3834  iunxsng  3835  iunxsngf  3837  cbvdisj  3862  disjnim  3866  disjiun  3870  mpteq12f  3948  axpweq  4035  rabxfrd  4328  onsucelsucexmid  4383  ordsucunielexmid  4384  0elsucexmid  4418  0nelelxp  4506  opeliunxp  4532  opeliunxp2  4617  iunxpf  4625  elreimasng  4841  elimasng  4843  xpimasn  4923  ressn  5015  funfni  5159  fnbr  5161  fun11iun  5322  fvelrnb  5401  fvun1  5419  fvco2  5422  elfvmptrab1  5447  elfvmptrab  5448  elpreima  5471  dff3im  5497  resflem  5516  fmptco  5518  funfvima3  5583  foima2  5585  eluniimadm  5598  dff13  5601  f1eqcocnv  5624  isoini  5651  riotaeqdv  5663  mpoeq123dva  5764  cbvmpox  5781  ovelrn  5851  elovmpo  5903  fmpox  6028  disjxp1  6063  opeliunxp2f  6065  mpoxopn0yelv  6066  mpoxopovel  6068  rbropapd  6069  rntpos  6084  smoel  6127  smoiso  6129  smoel2  6130  tfrlem9  6146  tfrlemisucaccv  6152  tfrlemiubacc  6157  tfrlemi14d  6160  tfri2d  6163  tfr1onlemubacc  6173  tfr1onlemres  6176  tfrcllemubacc  6186  tfrcllemres  6189  rdgon  6213  freceq1  6219  freceq2  6220  frec0g  6224  frecabcl  6226  freccllem  6229  frecfcllem  6231  frecsuclem  6233  frecsuc  6234  nnsucelsuc  6317  nnsucuniel  6321  nnmordi  6342  ereldm  6402  iinerm  6431  elmapg  6485  elpmg  6488  elixpsn  6559  ixpsnf1o  6560  phplem4  6678  phplem3g  6679  phplem4on  6690  exmidpw  6731  fiintim  6746  fidcenumlemrks  6769  fidcenumlemrk  6770  ordiso2  6835  ctssdclemr  6911  archnqq  7126  ltdfpr  7215  genpelxp  7220  genpelvl  7221  genpelvu  7222  addcanprleml  7323  addcanprlemu  7324  cauappcvgprlem1  7368  eluz1  9180  elixx1  9521  elioo2  9545  elfz1  9636  elfzp1  9693  fzpr  9698  fzsuc2  9700  fzrev3  9708  elfzp12  9720  fzm1  9721  fzoval  9766  elfzo  9767  fzodcel  9770  elfzom1b  9847  fzosplitsni  9853  zmodidfzo  9967  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  bcval  10336  bcpasc  10353  shftfn  10437  shftval  10438  seq3shft  10451  iser3shft  10954  sumeq1  10963  summodclem3  10988  summodclem2a  10989  isumss  10999  fsumsplit  11015  sumsplitdc  11040  fsum2dlemstep  11042  fisumcom2  11046  fsumparts  11078  explecnv  11113  eftlub  11194  divalgmod  11419  algfx  11526  eucalgcvga  11532  ennnfonelemex  11719  ennnfonelemhom  11720  ennnfonelemf1  11723  ennnfonelemrn  11724  ctinfomlemom  11732  ctinfom  11733  elrest  11909  istopon  11962  eltg  12003  eltg2  12004  eltop  12020  eltop2  12021  eltop3  12022  iscld  12054  neiss2  12093  isnei  12095  lmfval  12143  cnfval  12145  iscn  12147  iscnp  12149  tgcn  12158  tgcnp  12159  lmbrf  12165  cnptopresti  12188  txbas  12208  eltx  12209  txdis  12227  txdis1cn  12228  ispsmet  12251  ismet  12272  isxmet  12273  elblps  12318  elbl  12319  elmopn  12374  neibl  12419  metrest  12434  metcnpd  12442  elcncf  12473  ellimc3ap  12511  cnlimcim  12517  eldvap  12524  bj-sels  12693  nninfalllemn  12786  nninfall  12788  nninfsellemeq  12794