Theorem eleq1a 2824

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  elex22  3475  disj  4416  disjne  4421  rabsneq  4611  elpr2g  4618  eqoreldif  4652  ordelinel  6438  onun2  6445  ssimaex  6949  fnex  7194  f1ocnv2d  7645  omun  7867  peano5  7872  mpoexw  8060  tfrlem8  8355  tz7.48-2  8413  tz7.49  8416  eroprf  8791  pssnn  9138  onfin  9185  ac6sfi  9238  elfiun  9388  brwdom  9527  ficardom  9921  ficard  10525  tskxpss  10732  inar1  10735  rankcf  10737  tskuni  10743  gruun  10766  nsmallnq  10937  prnmadd  10957  genpss  10964  mpoaddf  11169  mpomulf  11170  eqlei  11291  eqlei2  11292  renegcli  11490  supaddc  12157  supadd  12158  supmul1  12159  supmullem2  12161  supmul  12162  nn0ind-raph  12641  uzwo  12877  iccid  13358  hashvnfin  14332  hashdifsnp1  14478  mertenslem2  15858  4sqlem1  16926  4sqlem4  16930  4sqlem11  16933  symggen  19407  psgnran  19452  odlem1  19472  gexlem1  19516  gsumpr  19892  lssvneln0  20865  lss1d  20876  lspsn  20915  lsmelval2  20999  rnglidlmmgm  21162  psgnghm  21496  opnneiid  23020  cmpsublem  23293  metrest  24419  metustel  24445  dscopn  24468  ovolshftlem2  25418  subopnmbl  25512  deg1ldgn  26005  plyremlem  26219  coseq0negpitopi  26419  ppiublem1  27120  noextendseq  27586  bdayfo  27596  scutf  27731  addsproplem2  27884  mptelee  28829  nbuhgr2vtx1edgblem  29285  numclwwlk1lem2foa  30290  shsleji  31306  spansnss  31507  spansncvi  31588  f1o3d  32558  sigaclcu2  34117  measdivcstALTV  34222  dfon2lem6  35783  altxpsspw  35972  hfun  36173  ontgval  36426  ordtoplem  36430  ordcmp  36442  findreccl  36448  bj-xpnzex  36954  bj-snsetex  36958  bj-ismooredr2  37105  bj-ideqg1  37159  topdifinfindis  37341  finxpreclem1  37384  ovoliunnfl  37663  volsupnfl  37666  heibor1lem  37810  heibor1  37811  lshpkrlem1  39110  lfl1dim  39121  leat3  39295  meetat2  39297  glbconxN  39379  pointpsubN  39752  pmapglbx  39770  linepsubclN  39952  dia2dimlem7  41071  dib1dim2  41169  diclspsn  41195  dih1dimatlem  41330  dihatexv2  41340  djhlsmcl  41415  fsuppssind  42588  fltne  42639  3cubes  42685  hbtlem2  43120  hbtlem5  43124  rp-isfinite6  43514  snssiALTVD  44823  snssiALT  44824  elex2VD  44834  elex22VD  44835  upwordnul  46885  upwordsing  46889  tworepnotupword  46891  fveqvfvv  47045  afv0fv0  47154  lswn0  47449  1neven  48230  cznrng  48253