Theorem eleq1a 2725

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

Syntax hints:   → wi 4   = wceq 1523   ∈ wcel 2030

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647

This theorem is referenced by:  elex2  3247  elex22  3248  clel5  3375  reu6  3428  disjne  4055  eqoreldif  4257  ordelinel  5863  ssimaex  6302  fnex  6522  f1ocnv2d  6928  peano5  7131  tfrlem8  7525  tz7.48-2  7582  tz7.49  7585  eroprf  7888  onfin  8192  pssnn  8219  ac6sfi  8245  elfiun  8377  brwdom  8513  ficardom  8825  ficard  9425  tskxpss  9632  inar1  9635  rankcf  9637  tskuni  9643  gruun  9666  nsmallnq  9837  prnmadd  9857  genpss  9864  eqlei  10185  eqlei2  10186  renegcli  10380  supaddc  11028  supadd  11029  supmul1  11030  supmullem2  11032  supmul  11033  nn0ind-raph  11515  uzwo  11789  iccid  12258  hashvnfin  13189  brfi1indlem  13316  mertenslem2  14661  4sqlem1  15699  4sqlem4  15703  4sqlem11  15706  symggen  17936  psgnran  17981  odlem1  18000  gexlem1  18040  lssneln0  19000  lss1d  19011  lspsn  19050  lsmelval2  19133  psgnghm  19974  opnneiid  20978  cmpsublem  21250  metrest  22376  metustel  22402  dscopn  22425  ovolshftlem2  23324  subopnmbl  23418  deg1ldgn  23898  plyremlem  24104  coseq0negpitopi  24300  ppiublem1  24972  mptelee  25820  nbuhgr2vtx1edgblem  26292  clwwlknonwwlknonbOLD  27081  numclwlk1lem2foa  27344  shsleji  28357  spansnss  28558  spansncvi  28639  f1o3d  29559  sigaclcu2  30311  measdivcstOLD  30415  dfon2lem6  31817  noextendseq  31945  bdayfo  31953  scutf  32044  altxpsspw  32209  hfun  32410  ontgval  32555  ordtoplem  32559  ordcmp  32571  findreccl  32577  bj-xpnzex  33071  bj-snsetex  33076  topdifinfindis  33324  finxpreclem1  33356  ovoliunnfl  33581  volsupnfl  33584  heibor1lem  33738  heibor1  33739  lshpkrlem1  34715  lfl1dim  34726  leat3  34900  meetat2  34902  glbconxN  34982  pointpsubN  35355  pmapglbx  35373  linepsubclN  35555  dia2dimlem7  36676  dib1dim2  36774  diclspsn  36800  dih1dimatlem  36935  dihatexv2  36945  djhlsmcl  37020  hbtlem2  38011  hbtlem5  38015  rp-isfinite6  38181  snssiALTVD  39376  snssiALT  39377  elex2VD  39387  elex22VD  39388  fveqvfvv  41525  afv0fv0  41550  lswn0  41705  lidlmmgm  42250  1neven  42257  cznrng  42280  gsumpr  42464