Theorem eleq1a 2885

Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.)

Assertion

Ref	Expression
eleq1a	⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Proof of Theorem eleq1a

Step	Hyp	Ref	Expression
1		eleq1 2877	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 253	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  elex2  3463  elex22  3464  disj  4355  disjne  4362  elpr2g  4549  eqoreldif  4582  ordelinel  6257  ssimaex  6723  fnex  6957  f1ocnv2d  7378  peano5  7585  mpoexw  7759  tfrlem8  8003  tz7.48-2  8061  tz7.49  8064  eroprf  8378  onfin  8694  pssnn  8720  ac6sfi  8746  elfiun  8878  brwdom  9015  ficardom  9374  ficard  9976  tskxpss  10183  inar1  10186  rankcf  10188  tskuni  10194  gruun  10217  nsmallnq  10388  prnmadd  10408  genpss  10415  eqlei  10739  eqlei2  10740  renegcli  10936  supaddc  11595  supadd  11596  supmul1  11597  supmullem2  11599  supmul  11600  nn0ind-raph  12070  uzwo  12299  iccid  12771  hashvnfin  13717  hashdifsnp1  13850  mertenslem2  15233  4sqlem1  16274  4sqlem4  16278  4sqlem11  16281  symggen  18590  psgnran  18635  odlem1  18655  gexlem1  18696  gsumpr  19068  lssvneln0  19716  lss1d  19728  lspsn  19767  lsmelval2  19850  psgnghm  20269  opnneiid  21731  cmpsublem  22004  metrest  23131  metustel  23157  dscopn  23180  ovolshftlem2  24114  subopnmbl  24208  deg1ldgn  24694  plyremlem  24900  coseq0negpitopi  25096  ppiublem1  25786  mptelee  26689  nbuhgr2vtx1edgblem  27141  numclwwlk1lem2foa  28139  shsleji  29153  spansnss  29354  spansncvi  29435  f1o3d  30386  sigaclcu2  31489  measdivcstALTV  31594  dfon2lem6  33146  noextendseq  33287  bdayfo  33295  scutf  33386  altxpsspw  33551  hfun  33752  ontgval  33892  ordtoplem  33896  ordcmp  33908  findreccl  33914  bj-xpnzex  34395  bj-snsetex  34399  bj-ismooredr2  34525  bj-ideqg1  34579  topdifinfindis  34763  finxpreclem1  34806  ovoliunnfl  35099  volsupnfl  35102  heibor1lem  35247  heibor1  35248  lshpkrlem1  36406  lfl1dim  36417  leat3  36591  meetat2  36593  glbconxN  36674  pointpsubN  37047  pmapglbx  37065  linepsubclN  37247  dia2dimlem7  38366  dib1dim2  38464  diclspsn  38490  dih1dimatlem  38625  dihatexv2  38635  djhlsmcl  38710  fsuppssind  39459  fltne  39616  3cubes  39631  hbtlem2  40068  hbtlem5  40072  rp-isfinite6  40226  snssiALTVD  41533  snssiALT  41534  elex2VD  41544  elex22VD  41545  fveqvfvv  43632  afv0fv0  43705  lswn0  43961  lidlmmgm  44549  1neven  44556  cznrng  44579