Theorem eleq2d 2266

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 2260	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶 ∈ 𝐴 ↔ 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   ↔ wb 105   = wceq 1364   ∈ wcel 2167

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  eleq12d  2267  eleqtrd  2275  neleqtrd  2294  neleqtrrd  2295  abeq2d  2309  nfceqdf  2338  drnfc1  2356  drnfc2  2357  sbcbid  3047  cbvcsbw  3088  cbvcsb  3089  sbcel1g  3103  csbeq2d  3109  csbie2g  3135  cbvralcsf  3147  cbvrexcsf  3148  cbvreucsf  3149  cbvrabcsf  3150  opeq1  3809  opeq2  3810  cbviun  3954  cbviin  3955  iinxsng  3991  iinxprg  3992  iunxsng  3993  iunxsngf  3995  cbvdisj  4021  disjnim  4025  disjiun  4029  mpteq12f  4114  axpweq  4205  rabxfrd  4505  onsucelsucexmid  4567  ordsucunielexmid  4568  0elsucexmid  4602  0nelelxp  4693  opeliunxp  4719  opeliunxp2  4807  iunxpf  4815  elrelimasn  5036  elimasng  5038  xpimasn  5119  ressn  5211  funfni  5361  fnbr  5363  fun11iun  5528  fvelrnb  5611  foelcdmi  5616  fvun1  5630  fvco2  5633  elfvmptrab1  5659  elfvmptrab  5660  elpreima  5684  dff3im  5710  resflem  5729  fmptco  5731  funfvima3  5799  foima2  5801  eluniimadm  5815  dff13  5818  f1eqcocnv  5841  isoini  5868  riotaeqdv  5881  mpoeq123dva  5987  cbvmpox  6004  ovelrn  6076  elovmpod  6125  elovmpo  6126  elovmporab  6127  elovmporab1w  6128  fmpox  6267  disjxp1  6303  opeliunxp2f  6305  mpoxopn0yelv  6306  mpoxopovel  6308  rbropapd  6309  rntpos  6324  smoel  6367  smoiso  6369  smoel2  6370  tfrlem9  6386  tfrlemisucaccv  6392  tfrlemiubacc  6397  tfrlemi14d  6400  tfri2d  6403  tfr1onlemubacc  6413  tfr1onlemres  6416  tfrcllemubacc  6426  tfrcllemres  6429  rdgon  6453  freceq1  6459  freceq2  6460  frec0g  6464  frecabcl  6466  freccllem  6469  frecfcllem  6471  frecsuclem  6473  frecsuc  6474  nnsucelsuc  6558  nnsucuniel  6562  nnmordi  6583  ereldm  6646  iinerm  6675  elmapg  6729  elpmg  6732  elixpsn  6803  ixpsnf1o  6804  pw2f1odclem  6904  phplem4  6925  phplem3g  6926  phplem4on  6937  exmidpw  6978  fiintim  7001  fidcenumlemrks  7028  fidcenumlemrk  7029  elfi  7046  ordiso2  7110  ctssdccl  7186  nnnninfeq  7203  cc2lem  7351  cc2  7352  cc3  7353  archnqq  7503  ltdfpr  7592  genpelxp  7597  genpelvl  7598  genpelvu  7599  addcanprleml  7700  addcanprlemu  7701  cauappcvgprlem1  7745  suplocexprlemell  7799  suplocexprlemmu  7804  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  cnm  7918  eluz1  9624  elixx1  9991  elioo2  10015  elfz1  10107  elfzp1  10166  fzpr  10171  fzsuc2  10173  fzrev3  10181  elfzp12  10193  fzm1  10194  fzoval  10242  elfzo  10243  fzodcel  10247  elfzom1b  10324  fzosplitsni  10330  nninfdcex  10346  zmodidfzo  10464  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  seqf1og  10632  bcval  10860  bcpasc  10877  wrdmap  10985  elovmpowrd  10995  shftfn  11008  shftval  11009  seq3shft  11022  iser3shft  11530  sumeq1  11539  summodclem3  11564  summodclem2a  11565  isumss  11575  fsumsplit  11591  sumsplitdc  11616  fsum2dlemstep  11618  fisumcom2  11622  fsumparts  11654  explecnv  11689  fprodsplitdc  11780  fprodsplit  11781  fprod2dlemstep  11806  fprodcom2fi  11810  eftlub  11874  divalgmod  12111  bitsval  12127  bitsp1e  12136  bitsp1o  12137  algfx  12247  eucalgcvga  12253  reumodprminv  12449  nnnn0modprm0  12451  ennnfonelemex  12658  ennnfonelemhom  12659  ennnfonelemf1  12662  ennnfonelemrn  12663  ctinfomlemom  12671  ctinfom  12672  ctiunctlemudc  12681  ctiunctlemf  12682  elrest  12950  ptex  12968  prdsbasmpt  12984  prdsbasmpt2  12992  pwselbasb  12997  imasaddfnlemg  13018  divsfval  13032  xpscf  13051  grpidvalg  13077  grpidpropdg  13078  grpidd  13087  issgrpd  13116  sgrppropd  13117  ismndd  13141  mndpropd  13144  imasmnd2  13156  imasmnd  13157  ismhm  13165  issubm  13176  imasgrp2  13318  imasgrp  13319  issubg  13381  subginv  13389  isnsg  13410  eqg0el  13437  quselbasg  13438  isghm  13451  resghm2b  13470  conjnmzb  13488  conjnsg  13489  ghmpropd  13491  imasabl  13544  isrngd  13587  rngpropd  13589  imasrng  13590  qusrng  13592  dfur2g  13596  srgidmlem  13612  issrgid  13615  ringcl  13647  isringid  13659  isringd  13675  imasring  13698  oppr0g  13715  oppr1g  13716  reldvdsrsrg  13726  dvdsrvald  13727  isunitd  13740  unitinvcl  13757  unitinvinv  13758  unitlinv  13760  unitrinv  13761  unitnegcl  13764  dvdsrpropdg  13781  isrhm  13792  isrim0  13795  rhmmul  13798  islring  13826  issubrng  13833  opprsubrngg  13845  issubrg  13855  resrhm2b  13883  rhmpropd  13888  rrgval  13896  aprval  13916  aprap  13920  islmod  13925  lmodprop2d  13982  islssm  13991  islssmg  13992  islssmd  13993  lssats2  14048  ellspsn  14051  ixpsnbasval  14100  islidlm  14113  isridlrng  14116  rspssp  14128  rnglidlmmgm  14130  2idlval  14136  isridl  14138  2idlelb  14139  quscrng  14167  rspsn  14168  zrhval  14251  zrhrhmb  14256  znf1o  14285  psrgrp  14319  mplelbascoe  14326  istopon  14357  eltg  14396  eltg2  14397  eltop  14413  eltop2  14414  eltop3  14415  iscld  14447  neiss2  14486  isnei  14488  lmfval  14536  cnfval  14538  iscn  14541  iscnp  14543  tgcn  14552  tgcnp  14553  lmbrf  14559  cnptopresti  14582  txbas  14602  eltx  14603  txdis  14621  txdis1cn  14622  hmeofvalg  14647  ishmeo  14648  ispsmet  14667  ismet  14688  isxmet  14689  elblps  14734  elbl  14735  elmopn  14790  neibl  14835  metrest  14850  txmetcnp  14862  txmetcn  14863  metcnpd  14864  elcncf  14917  ellimc3apf  15004  limcmpted  15007  cnlimcim  15015  cnlimc  15016  eldvap  15026  dvidsslem  15037  dviaddf  15049  dvimulf  15050  elply  15078  ply1termlem  15086  lgseisenlem3  15421  bj-sels  15668  2omap  15750  nninfall  15764  nninfsellemeq  15769