Theorem eleq1a 2696

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 2689	. 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2	1	biimprcd 240	1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵))

Syntax hints:   → wi 4   = wceq 1483   ∈ wcel 1990

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-clel 2618

This theorem is referenced by:  elex2  3216  elex22  3217  clel5  3343  reu6  3395  disjne  4022  eqoreldif  4225  ordelinel  5825  ssimaex  6263  fnex  6481  f1ocnv2d  6886  peano5  7089  tfrlem8  7480  tz7.48-2  7537  tz7.49  7540  eroprf  7845  onfin  8151  pssnn  8178  ac6sfi  8204  elfiun  8336  brwdom  8472  ficardom  8787  ficard  9387  tskxpss  9594  inar1  9597  rankcf  9599  tskuni  9605  gruun  9628  nsmallnq  9799  prnmadd  9819  genpss  9826  eqlei  10147  eqlei2  10148  renegcli  10342  supaddc  10990  supadd  10991  supmul1  10992  supmullem2  10994  supmul  10995  nn0ind-raph  11477  uzwo  11751  iccid  12220  hashvnfin  13151  brfi1indlem  13278  mertenslem2  14617  4sqlem1  15652  4sqlem4  15656  4sqlem11  15659  symggen  17890  psgnran  17935  odlem1  17954  gexlem1  17994  lssneln0  18952  lss1d  18963  lspsn  19002  lsmelval2  19085  psgnghm  19926  opnneiid  20930  cmpsublem  21202  metrest  22329  metustel  22355  dscopn  22378  ovolshftlem2  23278  subopnmbl  23372  deg1ldgn  23853  plyremlem  24059  coseq0negpitopi  24255  ppiublem1  24927  mptelee  25775  nbuhgr2vtx1edgblem  26247  numclwlk1lem2foa  27224  shsleji  28229  spansnss  28430  spansncvi  28511  f1o3d  29431  sigaclcu2  30183  measdivcstOLD  30287  dfon2lem6  31693  noextendseq  31820  bdayfo  31828  scutf  31919  altxpsspw  32084  hfun  32285  ontgval  32430  ordtoplem  32434  ordcmp  32446  findreccl  32452  bj-xpnzex  32946  bj-snsetex  32951  topdifinfindis  33194  finxpreclem1  33226  ovoliunnfl  33451  volsupnfl  33454  heibor1lem  33608  heibor1  33609  lshpkrlem1  34397  lfl1dim  34408  leat3  34582  meetat2  34584  glbconxN  34664  pointpsubN  35037  pmapglbx  35055  linepsubclN  35237  dia2dimlem7  36359  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  dihatexv2  36628  djhlsmcl  36703  hbtlem2  37694  hbtlem5  37698  rp-isfinite6  37864  snssiALTVD  39062  snssiALT  39063  elex2VD  39073  elex22VD  39074  fveqvfvv  41204  afv0fv0  41229  lswn0  41380  lidlmmgm  41925  1neven  41932  cznrng  41955  gsumpr  42139