Theorem eleq2d 1156

Description: Deduction from equality to equivalence of membership.

Hypothesis

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

Assertion

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

Proof of Theorem eleq2d

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

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

This theorem is referenced by:  eleq12d 1157  eleqtrd 1165  cleqabd 1178  opprc1b 1906  cbviunv 2016  iunxsn 2034  eqelsuc 2307  eliniseg 2618  funfni 2724  fnbr 2726  fneu 2728  zfrep6 2744  fniunfv 2860  cleqfv 2880  funfvima3 2906  f1fv 2916  isoini 2938  tfrlem9 2957  tfrlem10 2958  tfrlem11 2959  oalimcl 3162  oaass 3163  omordi 3164  oen0 3165  omsmolem 3195  phplem5 3407  php3 3411  inf0 3457  inf3lemd 3463  inf3lem1 3464  inf3lem2 3465  inf3lem3 3466  trcl 3489  r1tr 3498  r1ord 3499  tz9.12lem3 3505  tz9.12 3506  rankval2 3514  rankid 3516  rankr1 3518  rankval3 3525  r1pwcl 3530  aceq3 3556  aceq5lem5 3562  aceq5 3563  kmlem2 3581  kmlem11 3590  kmlem12 3591  kmlem14 3593  zornlem1 3603  zorn 3611  alephnbtwn 3674  cardaleph 3690  cardinfima 3696  genpelv 3897  genpprecl 3898  genpnnp 3902  ruclem37 4921  infxpidmlem5 4937  ocelt 5162  shselt 5280  shsel2t 5287  shmods 5363  elspan 5449  h1de2ctlem 5460  elspansnt 5471  elspansn2t 5472

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