Theorem eleq1a 1158

Description: A transitive-type law relating membership and equality.

Assertion

Ref	Expression
eleq1a	⊢ (A ∈ B → (C = A → C ∈ B))

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 1149	. 2 ⊢ (C = A → (C ∈ B ↔ A ∈ B))
2	1	biimprcd 138	1 ⊢ (A ∈ B → (C = A → C ∈ B))

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

This theorem is referenced by:  prss 1854  tpss 1855  ordtr2 2257  peano5 2394  fopab2 2891  iunon 2947  iinon 2948  tz7.48-2 2995  tz7.49 2997  en3d 3304  onfin 3415  pssnn 3428  rankr1 3518  cardnn 3631  genpss 3901  distrlem1pr 3921  renegcl 4171  redivcl 4274  uzwo 4605  nnwoOLD 4608  nn0ind 4612  chocuni 5179  shselt 5280  spansn 5462  spansncv 5542

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