Theorem eleq1a 2831

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  elex22  3454  disjne  4395  rabsneq  4586  elpr2g  4593  eqoreldif  4629  ordelinel  6426  onun2  6433  ssimaex  6925  fnex  7172  f1ocnv2d  7620  omun  7839  peano5  7844  mpoexw  8031  tfrlem8  8323  tz7.48-2  8381  tz7.49  8384  eroprf  8762  pssnn  9103  onfin  9149  ac6sfi  9194  elfiun  9343  brwdom  9482  ficardom  9885  ficard  10487  tskxpss  10695  inar1  10698  rankcf  10700  tskuni  10706  gruun  10729  nsmallnq  10900  prnmadd  10920  genpss  10927  mpoaddf  11132  mpomulf  11133  eqlei  11256  eqlei2  11257  renegcli  11455  supaddc  12123  supadd  12124  supmul1  12125  supmullem2  12127  supmul  12128  nn0ind-raph  12629  uzwo  12861  iccid  13343  hashvnfin  14322  hashdifsnp1  14468  mertenslem2  15850  4sqlem1  16919  4sqlem4  16923  4sqlem11  16926  symggen  19445  psgnran  19490  odlem1  19510  gexlem1  19554  gsumpr  19930  lssvneln0  20947  lss1d  20958  lspsn  20997  lsmelval2  21080  rnglidlmmgm  21243  psgnghm  21560  opnneiid  23091  cmpsublem  23364  metrest  24489  metustel  24515  dscopn  24538  ovolshftlem2  25477  subopnmbl  25571  deg1ldgn  26058  plyremlem  26270  coseq0negpitopi  26467  ppiublem1  27165  noextendseq  27631  bdayfo  27641  cutsf  27784  addsproplem2  27962  mpteleeOLD  28964  nbuhgr2vtx1edgblem  29420  numclwwlk1lem2foa  30424  shsleji  31441  spansnss  31642  spansncvi  31723  f1o3d  32699  sigaclcu2  34264  measdivcstALTV  34369  dfon2lem6  35968  altxpsspw  36159  hfun  36360  ontgval  36613  ordtoplem  36617  ordcmp  36629  findreccl  36635  bj-xpnzex  37266  bj-snsetex  37270  bj-ismooredr2  37422  bj-ideqg1  37478  topdifinfindis  37662  finxpreclem1  37705  ovoliunnfl  37983  volsupnfl  37986  heibor1lem  38130  heibor1  38131  lshpkrlem1  39556  lfl1dim  39567  leat3  39741  meetat2  39743  glbconxN  39824  pointpsubN  40197  pmapglbx  40215  linepsubclN  40397  dia2dimlem7  41516  dib1dim2  41614  diclspsn  41640  dih1dimatlem  41775  dihatexv2  41785  djhlsmcl  41860  fsuppssind  43026  fltne  43077  3cubes  43122  hbtlem2  43552  hbtlem5  43556  rp-isfinite6  43945  snssiALTVD  45253  snssiALT  45254  elex2VD  45264  elex22VD  45265  fveqvfvv  47488  afv0fv0  47597  lswn0  47904  1neven  48714  cznrng  48737