Theorem eleq1d 1155

Description: Deduction from equality to equivalence of membership.

Hypothesis

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

Assertion

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

Proof of Theorem eleq1d

Step	Hyp	Ref	Expression
1		eleq1d.1	. 2 ⊢ (φ → A = B)
2		eleq1 1149	. 2 ⊢ (A = B → (A ∈ C ↔ B ∈ C))
3	1, 2	syl 12	1 ⊢ (φ → (A ∈ C ↔ B ∈ C))

Syntax hints:   → wi 2   ↔ wb 127   = wceq 1091   ∈ wcel 1092

This theorem is referenced by:  eleq12d 1157  eqeltrd 1163  inex1g 1699  class2set 1747  pwex 1806  pwexg 1807  snex 1859  moabex 1868  prex 1892  uniex 1947  uniexg 1948  unexb 1950  intex 1986  breq1 2065  breq2 2066  brprc 2097  opabsb 2114  opelopabg 2115  onint 2261  trsuc 2308  limsuc 2361  nlimsuc 2363  opelxp 2452  opelxpg 2454  relsn 2485  xpexg 2489  opelcog 2511  dfdmf 2526  eldmg 2529  opeldm 2534  elreldm 2554  dfrnf 2561  elrn 2562  iss 2599  imasn 2616  elimasn 2617  intirr 2628  cnvopab 2632  funimaexg 2715  fnex 2740  zfrep6 2744  fnopabg 2745  fcoi1 2765  fcoi2 2766  fornex 2793  tz6.12f 2844  ndmfvrcl 2849  funopfvg 2854  dmfco 2864  fvco 2865  fvopabn 2873  funopfv 2886  fvrn 2888  fopab2 2891  fsn 2895  fressnfv 2898  funfvima 2904  funfvima3 2906  abrexexg 2913  tfrlem9 2957  tz7.48-2 2995  abianfp 3000  ffnoprval 3041  ndmoprcl 3058  ndmoprrcl 3060  caoprcl 3066  f1stres 3096  oesuc 3134  oacl 3138  omcl 3139  oecl 3140  oaord1 3153  omordi 3164  oen0 3165  nnacl 3172  nnmcl 3173  nnmordi 3188  omsmolem 3195  ec2 3203  ecelqsi 3229  mapprc 3260  breng 3280  brdomg 3281  fundmen 3333  xpsnen 3339  pw2en 3348  mapxpen 3390  xpmapenlem5 3395  unblem2 3432  fiint 3445  dfom3 3477  rankon 3515  r1pw 3529  ranksn 3532  aceq3lem 3555  aceq4 3557  aceq5lem1 3558  aceq5lem5 3562  aceq6a 3564  aceq6b 3565  ac6lem 3575  numthlem 3598  zornlem1 3603  oncardon 3627  oncardid 3628  alephon 3671  cardcf 3706  addnidpi 3822  indpi 3828  addclpq 3852  mulclpq 3854  recclpq 3866  addclprlem2 3913  mulclprlem 3915  distrlem4pr 3924  prlem934a 3931  prlem934 3933  ltexprlem3 3938  ltexprlem4 3939  ltexprlem7 3942  ltexpri 3943  prlem936 3949  reclem1pr 3950  reclem2pr 3951  reclem3pr 3952  addclsr 3986  mulclsr 3987  suppsr 4016  suppsr2 4017  supsrlem4 4022  supsr 4025  supre 4054  axaddcl 4066  axaddrcl 4067  axmulcl 4068  axmulrcl 4069  axsup 4088  subclt 4140  renegclt 4172  divclz 4222  divclt 4223  redivclz 4275  redivclt 4276  peano2nn 4433  nnaddclt 4436  nnmulclt 4437  nnsub 4450  nnsubt 4451  crulem 4528  nn0mulclt 4554  elz 4565  nnnegz 4566  nn0subt 4587  znegclt 4588  zaddclt 4590  elnn0nn 4593  elnnnn0 4594  zmulclt 4596  zneo 4601  om2uzuz 4653  seqrn 4673  expcllem 4682  nneo 4719  sqrlem21 4751  sqrcl 4758  sqrclt 4767  sqr2irrlem2 4778  reim0 4809  absclt 4848  facclt 4874  ruclem13 4897  ruclem33 4917  ruclem35 4919  znnen 4930  shaddclt 5123  shmulclt 5124  hlimcaui 5141  hsn0elch 5155  occlt 5189  projlem10 5202  omlsilem 5249  pjoc1 5268  pjoml 5271  shsclt 5283  shintclt 5295  chintclt 5297  hsupclt 5308  shinclt 5352  chinclt 5416  h1datom 5483  osumlem8 5537  spansncv 5542  5oalem2 5545  5oalem3 5546  pjin 5584  pjjs 5585  pjclem4 5653  pj3s 5659  strlem1 5691  atcv0eq 5767  atcv1 5768  atcvatlem 5770

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-gen 677  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-cleq 1097  df-clel 1099

metamath.org