Theorem eleq1i 1152

Description: Inference from equality to equivalence of membership.

Hypothesis

Ref	Expression
eleq1i.1	⊢ A = B

Assertion

Ref	Expression
eleq1i	⊢ (A ∈ C ↔ B ∈ C)

Proof of Theorem eleq1i

Step	Hyp	Ref	Expression
1		eleq1i.1	. 2 ⊢ A = B
2		eleq1 1149	. 2 ⊢ (A = B → (A ∈ C ↔ B ∈ C))
3	1, 2	ax-mp 6	1 ⊢ (A ∈ C ↔ B ∈ C)

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

This theorem is referenced by:  eleq12i 1154  eqeltr 1159  difex2 1951  reucl 1957  reuuni3 1958  pwexb 1963  intexrab 1988  supcl 2159  ordtri3or 2230  sucexb 2301  xpex 2488  dmresexg 2586  resexg 2597  cnvexg 2669  resfunexg 2717  fressnfv 2898  iunon 2947  iinon 2948  tz7.48-3 2996  elxp6 3093  f1stres 3096  2o 3110  ecexg 3204  fiint 3445  inf3lem7 3470  r1pw 3529  scott0 3542  zornlem4 3606  htalem 3618  alephprc 3698  addclprlem2 3913  distrlem1pr 3921  distrlem2pr 3922  supsrlem5 4023  axicn 4065  negclt 4141  nn0subt 4587  uzwo3lem2 4615  seqrn 4673  discrlem2 4714  discrlem3 4715  nnesq 4720  reim0 4809  ruclem34 4918  pjthlem2 5226  pjthlem4 5228  pjoc1 5268  osum 5538  pjss2 5571  pjssm 5572

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