Theorem eleq1a 2855

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  elex22  3474  disjne  4408  rabsneq  4603  elpr2g  4610  eqoreldif  4646  ordelinel  6461  onun2  6468  ssimaex  6963  fnex  7216  f1ocnv2d  7667  omun  7884  peano5  7890  mpoexw  8077  tfrlem8  8373  tz7.48-2  8431  tz7.49  8434  eroprf  8815  pssnn  9163  onfin  9209  ac6sfi  9254  elfiun  9400  brwdom  9539  ficardom  9966  ficard  10573  tskxpss  10781  inar1  10784  rankcf  10786  tskuni  10792  gruun  10815  nsmallnq  10986  prnmadd  11006  genpss  11013  mpoaddf  11218  mpomulf  11219  eqlei  11344  eqlei2  11345  renegcli  11543  supaddc  12206  supadd  12207  supmul1  12208  supmullem2  12210  supmul  12211  nn0ind-raph  12721  uzwo  12960  iccid  13443  hashvnfin  14424  hashdifsnp1  14571  mertenslem2  15974  4sqlem1  17040  4sqlem4  17044  4sqlem11  17047  symggen  19597  psgnran  19642  odlem1  19662  gexlem1  19706  gsumpr  20082  lssvneln0  21136  lss1d  21147  lspsn  21186  lsmelval2  21269  rnglidlmmgm  21442  psgnghm  21793  opnneiid  23351  cmpsublem  23624  metrest  24750  metustel  24776  dscopn  24799  ovolshftlem2  25738  subopnmbl  25832  deg1ldgn  26318  plyremlem  26534  coseq0negpitopi  26741  ppiublem1  27438  noextendseq  27903  bdayfo  27913  cutsf  28057  addsproplem2  28235  mpteleeOLD  29352  nbuhgr2vtx1edgblem  29811  numclwwlk1lem2foa  30834  shsleji  31851  spansnss  32052  spansncvi  32133  f1o3d  33099  sigaclcu2  34630  measdivcstALTV  34736  kardfi  35696  dfon2lem6  36365  altxpsspw  36557  hfun  36758  ontgval  37050  ordtoplem  37054  ordcmp  37066  findreccl  37072  bj-xpnzex  37703  bj-snsetex  37707  bj-ismooredr2  37860  bj-ideqg1  37916  topdifinfindis  38100  finxpreclem1  38143  ovoliunnfl  38411  volsupnfl  38414  heibor1lem  38559  heibor1  38560  lshpkrlem1  39983  lfl1dim  39994  leat3  40168  meetat2  40170  glbconxN  40251  pointpsubN  40624  pmapglbx  40642  linepsubclN  40824  dia2dimlem7  41943  dib1dim2  42041  diclspsn  42067  dih1dimatlem  42202  dihatexv2  42212  djhlsmcl  42287  fsuppssind  43439  fltne  43490  3cubes  43535  hbtlem2  43965  hbtlem5  43969  rp-isfinite6  44358  snssiALTVD  45649  snssiALT  45650  elex2VD  45660  elex22VD  45661  fveqvfvv  47928  afv0fv0  48037  lswn0  48344  1neven  49153  cznrng  49176