Theorem eleq2d 2210

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

Syntax hints:   → wi 4   ↔ wb 104   = wceq 1332   ∈ wcel 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-clel 2136

This theorem is referenced by:  eleq12d  2211  eleqtrd  2219  neleqtrd  2238  neleqtrrd  2239  abeq2d  2253  nfceqdf  2281  drnfc1  2299  drnfc2  2300  sbcbid  2970  cbvcsbw  3011  cbvcsb  3012  sbcel1g  3026  csbeq2d  3032  csbie2g  3055  cbvralcsf  3067  cbvrexcsf  3068  cbvreucsf  3069  cbvrabcsf  3070  opeq1  3713  opeq2  3714  cbviun  3858  cbviin  3859  iinxsng  3894  iinxprg  3895  iunxsng  3896  iunxsngf  3898  cbvdisj  3924  disjnim  3928  disjiun  3932  mpteq12f  4016  axpweq  4103  rabxfrd  4398  onsucelsucexmid  4453  ordsucunielexmid  4454  0elsucexmid  4488  0nelelxp  4576  opeliunxp  4602  opeliunxp2  4687  iunxpf  4695  elreimasng  4913  elimasng  4915  xpimasn  4995  ressn  5087  funfni  5231  fnbr  5233  fun11iun  5396  fvelrnb  5477  fvun1  5495  fvco2  5498  elfvmptrab1  5523  elfvmptrab  5524  elpreima  5547  dff3im  5573  resflem  5592  fmptco  5594  funfvima3  5659  foima2  5661  eluniimadm  5674  dff13  5677  f1eqcocnv  5700  isoini  5727  riotaeqdv  5739  mpoeq123dva  5840  cbvmpox  5857  ovelrn  5927  elovmpo  5979  fmpox  6106  disjxp1  6141  opeliunxp2f  6143  mpoxopn0yelv  6144  mpoxopovel  6146  rbropapd  6147  rntpos  6162  smoel  6205  smoiso  6207  smoel2  6208  tfrlem9  6224  tfrlemisucaccv  6230  tfrlemiubacc  6235  tfrlemi14d  6238  tfri2d  6241  tfr1onlemubacc  6251  tfr1onlemres  6254  tfrcllemubacc  6264  tfrcllemres  6267  rdgon  6291  freceq1  6297  freceq2  6298  frec0g  6302  frecabcl  6304  freccllem  6307  frecfcllem  6309  frecsuclem  6311  frecsuc  6312  nnsucelsuc  6395  nnsucuniel  6399  nnmordi  6420  ereldm  6480  iinerm  6509  elmapg  6563  elpmg  6566  elixpsn  6637  ixpsnf1o  6638  phplem4  6757  phplem3g  6758  phplem4on  6769  exmidpw  6810  fiintim  6825  fidcenumlemrks  6849  fidcenumlemrk  6850  elfi  6867  ordiso2  6928  ctssdccl  7004  cc2lem  7098  cc2  7099  cc3  7100  archnqq  7249  ltdfpr  7338  genpelxp  7343  genpelvl  7344  genpelvu  7345  addcanprleml  7446  addcanprlemu  7447  cauappcvgprlem1  7491  suplocexprlemell  7545  suplocexprlemmu  7550  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  suplocexprlemlub  7556  cnm  7664  eluz1  9354  elixx1  9710  elioo2  9734  elfz1  9826  elfzp1  9883  fzpr  9888  fzsuc2  9890  fzrev3  9898  elfzp12  9910  fzm1  9911  fzoval  9956  elfzo  9957  fzodcel  9960  elfzom1b  10037  fzosplitsni  10043  zmodidfzo  10157  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  bcval  10527  bcpasc  10544  shftfn  10628  shftval  10629  seq3shft  10642  iser3shft  11147  sumeq1  11156  summodclem3  11181  summodclem2a  11182  isumss  11192  fsumsplit  11208  sumsplitdc  11233  fsum2dlemstep  11235  fisumcom2  11239  fsumparts  11271  explecnv  11306  eftlub  11433  divalgmod  11660  algfx  11769  eucalgcvga  11775  ennnfonelemex  11963  ennnfonelemhom  11964  ennnfonelemf1  11967  ennnfonelemrn  11968  ctinfomlemom  11976  ctinfom  11977  ctiunctlemudc  11986  ctiunctlemf  11987  elrest  12166  istopon  12219  eltg  12260  eltg2  12261  eltop  12277  eltop2  12278  eltop3  12279  iscld  12311  neiss2  12350  isnei  12352  lmfval  12400  cnfval  12402  iscn  12405  iscnp  12407  tgcn  12416  tgcnp  12417  lmbrf  12423  cnptopresti  12446  txbas  12466  eltx  12467  txdis  12485  txdis1cn  12486  hmeofvalg  12511  ishmeo  12512  ispsmet  12531  ismet  12552  isxmet  12553  elblps  12598  elbl  12599  elmopn  12654  neibl  12699  metrest  12714  txmetcnp  12726  txmetcn  12727  metcnpd  12728  elcncf  12768  ellimc3apf  12837  limcmpted  12840  cnlimcim  12848  cnlimc  12849  eldvap  12859  dviaddf  12877  dvimulf  12878  bj-sels  13283  nninfalllemn  13377  nninfall  13379  nninfsellemeq  13385