Theorem eleq1a 1586

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 1577	. 2 ⊢ (C = A → (C ∈ B ↔ A ∈ B))
2	1	biimprcd 154	1 ⊢ (A ∈ B → (C = A → C ∈ B))

Syntax hints:   → wi 3   = wceq 992   ∈ wcel 994

This theorem is referenced by:  reu3 1977  uniiunlem 2184  prss 2536  tpss 2541  ordtr2 3019  peano5 3241  ssimaex 3879  fopab2 3937  iunon 4207  iinon 4208  tfrlem8 4219  tz7.48-2 4258  tz7.49 4260  en3d 4542  onfin 4666  pssnn 4681  iunfi 4712  rankr1 4820  cardnn 4970  genpss 5261  distrlem1pr 5281  renegcli 5570  redivcli 5938  uzwo4OLD 6381  nn0ind-raph 6385  uzwo 6582  uzwoOLD 6583  climconsti 7297  opnneiid 7947  sncld 7997  cmsss 8208  chocunii 9448  shsel 9554  spansni 9756  spansncvi 9875  findreccl 10702  hmeogrp 11044  homcard 11045  qusp 11068  ccid 11412  compsublem 11487  ficard 11834  findcard 11836  fipreima 11848  inficl 11849  txsubsp 11983  heiborlem15 12025  heiborlem27 12037

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-cleq 1511  df-clel 1514

Copyright terms: Public domain